Metamath Proof Explorer

Theorem tngngp2

Description: A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngngp2.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngngp2.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
tngngp2.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
Assertion tngngp2 ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 tngngp2.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngngp2.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 tngngp2.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
4 ngpgrp ⊢ ( 𝑇 ∈ NrmGrp → 𝑇 ∈ Grp )
5 2 fvexi ⊢ 𝑋 ∈ V
6 reex ⊢ ℝ ∈ V
7 fex2 ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V ) → 𝑁 ∈ V )
8 5 6 7 mp3an23 ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → 𝑁 ∈ V )
9 2 a1i ⊢ ( 𝑁 ∈ V → 𝑋 = ( Base ‘ 𝐺 ) )
10 1 2 tngbas ⊢ ( 𝑁 ∈ V → 𝑋 = ( Base ‘ 𝑇 ) )
11 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
12 1 11 tngplusg ⊢ ( 𝑁 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
13 12 oveqdr ⊢ ( ( 𝑁 ∈ V ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
14 9 10 13 grppropd ⊢ ( 𝑁 ∈ V → ( 𝐺 ∈ Grp ↔ 𝑇 ∈ Grp ) )
15 8 14 syl ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝐺 ∈ Grp ↔ 𝑇 ∈ Grp ) )
16 4 15 syl5ibr ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp → 𝐺 ∈ Grp ) )
17 16 imp ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝐺 ∈ Grp )
18 ngpms ⊢ ( 𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp )
19 18 adantl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝑇 ∈ MetSp )
20 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
21 20 3 msmet2 ⊢ ( 𝑇 ∈ MetSp → ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) )
22 19 21 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) )
23 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
24 2 23 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
25 17 24 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
26 fco ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( -g ‘ 𝐺 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
27 25 26 syldan ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
28 8 adantr ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝑁 ∈ V )
29 1 23 tngds ⊢ ( 𝑁 ∈ V → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
30 28 29 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
31 3 30 eqtr4id ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝐷 = ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) )
32 31 feq1d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
33 27 32 mpbird ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
34 ffn ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ → 𝐷 Fn ( 𝑋 × 𝑋 ) )
35 fnresdm ⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
36 33 34 35 3syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
37 28 10 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝑋 = ( Base ‘ 𝑇 ) )
38 37 sqxpeqd ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝑋 × 𝑋 ) = ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) )
39 38 reseq2d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) )
40 36 39 eqtr3d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝐷 = ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) )
41 37 fveq2d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( Met ‘ 𝑋 ) = ( Met ‘ ( Base ‘ 𝑇 ) ) )
42 22 40 41 3eltr4d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
43 17 42 jca ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑇 ∈ NrmGrp ) → ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) )
44 15 biimpa ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝐺 ∈ Grp ) → 𝑇 ∈ Grp )
45 44 adantrr ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑇 ∈ Grp )
46 simprr ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
47 8 adantr ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑁 ∈ V )
48 47 10 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑋 = ( Base ‘ 𝑇 ) )
49 48 fveq2d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( Met ‘ 𝑋 ) = ( Met ‘ ( Base ‘ 𝑇 ) ) )
50 46 49 eleqtrd ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝐷 ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) )
51 metf ⊢ ( 𝐷 ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) → 𝐷 : ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ⟶ ℝ )
52 50 51 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝐷 : ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ⟶ ℝ )
53 ffn ⊢ ( 𝐷 : ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ⟶ ℝ → 𝐷 Fn ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) )
54 fnresdm ⊢ ( 𝐷 Fn ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) → ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) = 𝐷 )
55 52 53 54 3syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) = 𝐷 )
56 55 50 eqeltrd ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) )
57 55 fveq2d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( MetOpen ‘ ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) = ( MetOpen ‘ 𝐷 ) )
58 simprl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝐺 ∈ Grp )
59 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
60 1 3 59 tngtopn ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ V ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝑇 ) )
61 58 47 60 syl2anc ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝑇 ) )
62 57 61 eqtr2d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( TopOpen ‘ 𝑇 ) = ( MetOpen ‘ ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) )
63 eqid ⊢ ( TopOpen ‘ 𝑇 ) = ( TopOpen ‘ 𝑇 )
64 3 reseq1i ⊢ ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) = ( ( dist ‘ 𝑇 ) ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) )
65 63 20 64 isms2 ⊢ ( 𝑇 ∈ MetSp ↔ ( ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝑇 ) ) ∧ ( TopOpen ‘ 𝑇 ) = ( MetOpen ‘ ( 𝐷 ↾ ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ) ) ) )
66 56 62 65 sylanbrc ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑇 ∈ MetSp )
67 simpl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑁 : 𝑋 ⟶ ℝ )
68 1 2 6 tngnm ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 𝑁 = ( norm ‘ 𝑇 ) )
69 58 67 68 syl2anc ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑁 = ( norm ‘ 𝑇 ) )
70 9 10 eqtr3d ⊢ ( 𝑁 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
71 70 12 grpsubpropd ⊢ ( 𝑁 ∈ V → ( -g ‘ 𝐺 ) = ( -g ‘ 𝑇 ) )
72 47 71 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( -g ‘ 𝐺 ) = ( -g ‘ 𝑇 ) )
73 69 72 coeq12d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) )
74 47 29 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( 𝑁 ∘ ( -g ‘ 𝐺 ) ) = ( dist ‘ 𝑇 ) )
75 73 74 eqtr3d ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) = ( dist ‘ 𝑇 ) )
76 eqimss ⊢ ( ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) = ( dist ‘ 𝑇 ) → ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) ⊆ ( dist ‘ 𝑇 ) )
77 75 76 syl ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) ⊆ ( dist ‘ 𝑇 ) )
78 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
79 eqid ⊢ ( -g ‘ 𝑇 ) = ( -g ‘ 𝑇 )
80 eqid ⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
81 78 79 80 isngp ⊢ ( 𝑇 ∈ NrmGrp ↔ ( 𝑇 ∈ Grp ∧ 𝑇 ∈ MetSp ∧ ( ( norm ‘ 𝑇 ) ∘ ( -g ‘ 𝑇 ) ) ⊆ ( dist ‘ 𝑇 ) ) )
82 45 66 77 81 syl3anbrc ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) → 𝑇 ∈ NrmGrp )
83 43 82 impbida ⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Met ‘ 𝑋 ) ) ) )