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 syl5ibr ⊢ 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 50 51 syl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → D : Base T × Base T ⟶ ℝ
53 ffn ⊢ D : Base T × Base T ⟶ ℝ → D Fn Base T × Base T
54 fnresdm ⊢ D Fn Base T × Base T → D ↾ Base T × Base T = D
55 52 53 54 3syl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → D ↾ Base T × Base T = D
56 55 50 eqeltrd ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → D ↾ Base T × Base T ∈ Met ⁡ Base T
57 55 fveq2d ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → MetOpen ⁡ D ↾ Base T × Base T = MetOpen ⁡ D
58 simprl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → G ∈ Grp
59 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
60 1 3 59 tngtopn ⊢ G ∈ Grp ∧ N ∈ V → MetOpen ⁡ D = TopOpen ⁡ T
61 58 47 60 syl2anc ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → MetOpen ⁡ D = TopOpen ⁡ T
62 57 61 eqtr2d ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → TopOpen ⁡ T = MetOpen ⁡ D ↾ Base T × Base T
63 eqid ⊢ TopOpen ⁡ T = TopOpen ⁡ T
64 3 reseq1i ⊢ D ↾ Base T × Base T = dist ⁡ T ↾ Base T × Base T
65 63 20 64 isms2 ⊢ T ∈ MetSp ↔ D ↾ Base T × Base T ∈ Met ⁡ Base T ∧ TopOpen ⁡ T = MetOpen ⁡ D ↾ Base T × Base T
66 56 62 65 sylanbrc ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → T ∈ MetSp
67 simpl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → N : X ⟶ ℝ
68 1 2 6 tngnm ⊢ G ∈ Grp ∧ N : X ⟶ ℝ → N = norm ⁡ T
69 58 67 68 syl2anc ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → N = norm ⁡ T
70 9 10 eqtr3d ⊢ N ∈ V → Base G = Base T
71 70 12 grpsubpropd ⊢ N ∈ V → - G = - T
72 47 71 syl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → - G = - T
73 69 72 coeq12d ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → N ∘ - G = norm ⁡ T ∘ - T
74 47 29 syl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → N ∘ - G = dist ⁡ T
75 73 74 eqtr3d ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → norm ⁡ T ∘ - T = dist ⁡ T
76 eqimss ⊢ norm ⁡ T ∘ - T = dist ⁡ T → norm ⁡ T ∘ - T ⊆ dist ⁡ T
77 75 76 syl ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → norm ⁡ T ∘ - T ⊆ dist ⁡ T
78 eqid ⊢ norm ⁡ T = norm ⁡ T
79 eqid ⊢ - T = - T
80 eqid ⊢ dist ⁡ T = dist ⁡ T
81 78 79 80 isngp ⊢ T ∈ NrmGrp ↔ T ∈ Grp ∧ T ∈ MetSp ∧ norm ⁡ T ∘ - T ⊆ dist ⁡ T
82 45 66 77 81 syl3anbrc ⊢ N : X ⟶ ℝ ∧ G ∈ Grp ∧ D ∈ Met ⁡ X → T ∈ NrmGrp
83 43 82 impbida ⊢ N : X ⟶ ℝ → T ∈ NrmGrp ↔ G ∈ Grp ∧ D ∈ Met ⁡ X