This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tngds

Description: The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015) (Proof shortened by AV, 29-Oct-2024)

Ref Expression
Hypotheses tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngds.2 ⊢ − = ( -g ‘ 𝐺 )
Assertion tngds ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngds.2 ⊢ − = ( -g ‘ 𝐺 )
3 dsid ⊢ dist = Slot ( dist ‘ ndx )
4 dsndxntsetndx ⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx )
5 3 4 setsnid ⊢ ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) )
6 2 fvexi ⊢ − ∈ V
7 coexg ⊢ ( ( 𝑁 ∈ 𝑉 ∧ − ∈ V ) → ( 𝑁 ∘ − ) ∈ V )
8 6 7 mpan2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) ∈ V )
9 3 setsid ⊢ ( ( 𝐺 ∈ V ∧ ( 𝑁 ∘ − ) ∈ V ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) )
10 8 9 sylan2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) ) )
11 eqid ⊢ ( 𝑁 ∘ − ) = ( 𝑁 ∘ − )
12 eqid ⊢ ( MetOpen ‘ ( 𝑁 ∘ − ) ) = ( MetOpen ‘ ( 𝑁 ∘ − ) )
13 1 2 11 12 tngval ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → 𝑇 = ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) )
14 13 fveq2d ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( dist ‘ 𝑇 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( dist ‘ ndx ) , ( 𝑁 ∘ − ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑁 ∘ − ) ) ⟩ ) ) )
15 5 10 14 3eqtr4a ⊢ ( ( 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
16 co02 ⊢ ( 𝑁 ∘ ∅ ) = ∅
17 3 str0 ⊢ ∅ = ( dist ‘ ∅ )
18 16 17 eqtri ⊢ ( 𝑁 ∘ ∅ ) = ( dist ‘ ∅ )
19 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( -g ‘ 𝐺 ) = ∅ )
20 2 19 eqtrid ⊢ ( ¬ 𝐺 ∈ V → − = ∅ )
21 20 coeq2d ⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( 𝑁 ∘ ∅ ) )
22 reldmtng ⊢ Rel dom toNrmGrp
23 22 ovprc1 ⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 toNrmGrp 𝑁 ) = ∅ )
24 1 23 eqtrid ⊢ ( ¬ 𝐺 ∈ V → 𝑇 = ∅ )
25 24 fveq2d ⊢ ( ¬ 𝐺 ∈ V → ( dist ‘ 𝑇 ) = ( dist ‘ ∅ ) )
26 18 21 25 3eqtr4a ⊢ ( ¬ 𝐺 ∈ V → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
27 26 adantr ⊢ ( ( ¬ 𝐺 ∈ V ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
28 15 27 pm2.61ian ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )