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 ⊢ T = G toNrmGrp N
tngngp2.x ⊢ X = Base G
tngngp2.d ⊢ D = dist ⁡ T
Assertion tngngp2 ⊢ N : X ⟶ ℝ → T ∈ NrmGrp ↔ G ∈ Grp ∧ D ∈ Met ⁡ X

Proof

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