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=GtoNrmGrpN
tngngp2.x ⊢X=BaseG
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=GtoNrmGrpN
2 tngngp2.x ⊢X=BaseG
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=BaseG
10 1 2 tngbas ⊢N∈V→X=BaseT
11 eqid ⊢+G=+G
12 1 11 tngplusg ⊢N∈V→+G=+T
13 12 oveqdr ⊢N∈V∧x∈X∧y∈X→x+Gy=x+Ty
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 ⊢BaseT=BaseT
21 20 3 msmet2 ⊢T∈MetSp→D↾BaseT×BaseT∈Met⁡BaseT
22 19 21 syl ⊢N:X⟶ℝ∧T∈NrmGrp→D↾BaseT×BaseT∈Met⁡BaseT
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⟶ℝ→DFnX×X
35 fnresdm ⊢DFnX×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=BaseT
38 37 sqxpeqd ⊢N:X⟶ℝ∧T∈NrmGrp→X×X=BaseT×BaseT
39 38 reseq2d ⊢N:X⟶ℝ∧T∈NrmGrp→D↾X×X=D↾BaseT×BaseT
40 36 39 eqtr3d ⊢N:X⟶ℝ∧T∈NrmGrp→D=D↾BaseT×BaseT
41 37 fveq2d ⊢N:X⟶ℝ∧T∈NrmGrp→Met⁡X=Met⁡BaseT
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=BaseT
49 48 fveq2d ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→Met⁡X=Met⁡BaseT
50 46 49 eleqtrd ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→D∈Met⁡BaseT
51 metf ⊢D∈Met⁡BaseT→D:BaseT×BaseT⟶ℝ
52 50 51 syl ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→D:BaseT×BaseT⟶ℝ
53 ffn ⊢D:BaseT×BaseT⟶ℝ→DFnBaseT×BaseT
54 fnresdm ⊢DFnBaseT×BaseT→D↾BaseT×BaseT=D
55 52 53 54 3syl ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→D↾BaseT×BaseT=D
56 55 50 eqeltrd ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→D↾BaseT×BaseT∈Met⁡BaseT
57 55 fveq2d ⊢N:X⟶ℝ∧G∈Grp∧D∈Met⁡X→MetOpen⁡D↾BaseT×BaseT=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↾BaseT×BaseT
63 eqid ⊢TopOpen⁡T=TopOpen⁡T
64 3 reseq1i ⊢D↾BaseT×BaseT=dist⁡T↾BaseT×BaseT
65 63 20 64 isms2 ⊢T∈MetSp↔D↾BaseT×BaseT∈Met⁡BaseT∧TopOpen⁡T=MetOpen⁡D↾BaseT×BaseT
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→BaseG=BaseT
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