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

Metamath Proof Explorer

Theorem tngnm

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngnm.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngnm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngnm.a ⊢ 𝐴 ∈ V
Assertion tngnm ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( norm ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngnm.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngnm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 tngnm.a ⊢ 𝐴 ∈ V
4 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 : 𝑋 ⟶ 𝐴 )
5 4 feqmptd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑥 ) ) )
6 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
7 2 6 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
8 7 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
10 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
11 2 10 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
12 11 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
13 9 12 opelxpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ∈ ( 𝑋 × 𝑋 ) )
14 fvco3 ⊢ ( ( ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) ) )
15 8 13 14 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) ) )
16 df-ov ⊢ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ )
17 df-ov ⊢ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ )
18 17 fveq2i ⊢ ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑁 ‘ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , ( 0g ‘ 𝐺 ) ⟩ ) )
19 15 16 18 3eqtr4g ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) )
20 2 10 6 grpsubid1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
21 20 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
22 21 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 ( -g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑁 ‘ 𝑥 ) )
23 19 22 eqtr2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) )
24 23 mpteq2dva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) )
25 2 fvexi ⊢ 𝑋 ∈ V
26 fex2 ⊢ ( ( 𝑁 : 𝑋 ⟶ 𝐴 ∧ 𝑋 ∈ V ∧ 𝐴 ∈ V ) → 𝑁 ∈ V )
27 25 3 26 mp3an23 ⊢ ( 𝑁 : 𝑋 ⟶ 𝐴 → 𝑁 ∈ V )
28 27 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 ∈ V )
29 1 2 tngbas ⊢ ( 𝑁 ∈ V → 𝑋 = ( Base ‘ 𝑇 ) )
30 28 29 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑋 = ( Base ‘ 𝑇 ) )
31 1 6 tngds ⊢ ( 𝑁 ∈ V → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
32 28 31 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
33 eqidd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑥 = 𝑥 )
34 1 10 tng0 ⊢ ( 𝑁 ∈ V → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑇 ) )
35 28 34 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑇 ) )
36 32 33 35 oveq123d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) = ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) )
37 30 36 mpteq12dv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑇 ) ↦ ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) ) )
38 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
39 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
40 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
41 eqid ⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
42 38 39 40 41 nmfval ⊢ ( norm ‘ 𝑇 ) = ( 𝑥 ∈ ( Base ‘ 𝑇 ) ↦ ( 𝑥 ( dist ‘ 𝑇 ) ( 0g ‘ 𝑇 ) ) )
43 37 42 eqtr4di ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) ( 0g ‘ 𝐺 ) ) ) = ( norm ‘ 𝑇 ) )
44 5 24 43 3eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ 𝐴 ) → 𝑁 = ( norm ‘ 𝑇 ) )