Metamath Proof Explorer


Theorem tngngp

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngngp.t T = G toNrmGrp N
tngngp.x X = Base G
tngngp.m - ˙ = - G
tngngp.z 0 ˙ = 0 G
Assertion tngngp N : X T NrmGrp G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y

Proof

Step Hyp Ref Expression
1 tngngp.t T = G toNrmGrp N
2 tngngp.x X = Base G
3 tngngp.m - ˙ = - G
4 tngngp.z 0 ˙ = 0 G
5 eqid dist T = dist T
6 1 2 5 tngngp2 N : X T NrmGrp G Grp dist T Met X
7 6 simprbda N : X T NrmGrp G Grp
8 simplr N : X T NrmGrp x X T NrmGrp
9 simpr N : X T NrmGrp x X x X
10 2 fvexi X V
11 reex V
12 fex2 N : X X V V N V
13 10 11 12 mp3an23 N : X N V
14 13 ad2antrr N : X T NrmGrp x X N V
15 1 2 tngbas N V X = Base T
16 14 15 syl N : X T NrmGrp x X X = Base T
17 9 16 eleqtrd N : X T NrmGrp x X x Base T
18 eqid Base T = Base T
19 eqid norm T = norm T
20 eqid 0 T = 0 T
21 18 19 20 nmeq0 T NrmGrp x Base T norm T x = 0 x = 0 T
22 8 17 21 syl2anc N : X T NrmGrp x X norm T x = 0 x = 0 T
23 7 adantr N : X T NrmGrp x X G Grp
24 simpll N : X T NrmGrp x X N : X
25 1 2 11 tngnm G Grp N : X N = norm T
26 23 24 25 syl2anc N : X T NrmGrp x X N = norm T
27 26 fveq1d N : X T NrmGrp x X N x = norm T x
28 27 eqeq1d N : X T NrmGrp x X N x = 0 norm T x = 0
29 1 4 tng0 N V 0 ˙ = 0 T
30 14 29 syl N : X T NrmGrp x X 0 ˙ = 0 T
31 30 eqeq2d N : X T NrmGrp x X x = 0 ˙ x = 0 T
32 22 28 31 3bitr4d N : X T NrmGrp x X N x = 0 x = 0 ˙
33 simpllr N : X T NrmGrp x X y X T NrmGrp
34 17 adantr N : X T NrmGrp x X y X x Base T
35 16 eleq2d N : X T NrmGrp x X y X y Base T
36 35 biimpa N : X T NrmGrp x X y X y Base T
37 eqid - T = - T
38 18 19 37 nmmtri T NrmGrp x Base T y Base T norm T x - T y norm T x + norm T y
39 33 34 36 38 syl3anc N : X T NrmGrp x X y X norm T x - T y norm T x + norm T y
40 2 16 eqtr3id N : X T NrmGrp x X Base G = Base T
41 eqid + G = + G
42 1 41 tngplusg N V + G = + T
43 14 42 syl N : X T NrmGrp x X + G = + T
44 40 43 grpsubpropd N : X T NrmGrp x X - G = - T
45 3 44 syl5eq N : X T NrmGrp x X - ˙ = - T
46 45 oveqd N : X T NrmGrp x X x - ˙ y = x - T y
47 26 46 fveq12d N : X T NrmGrp x X N x - ˙ y = norm T x - T y
48 47 adantr N : X T NrmGrp x X y X N x - ˙ y = norm T x - T y
49 26 fveq1d N : X T NrmGrp x X N y = norm T y
50 27 49 oveq12d N : X T NrmGrp x X N x + N y = norm T x + norm T y
51 50 adantr N : X T NrmGrp x X y X N x + N y = norm T x + norm T y
52 39 48 51 3brtr4d N : X T NrmGrp x X y X N x - ˙ y N x + N y
53 52 ralrimiva N : X T NrmGrp x X y X N x - ˙ y N x + N y
54 32 53 jca N : X T NrmGrp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y
55 54 ralrimiva N : X T NrmGrp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y
56 7 55 jca N : X T NrmGrp G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y
57 simprl N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y G Grp
58 simpl N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y N : X
59 simpl N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y N x = 0 x = 0 ˙
60 59 ralimi x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y x X N x = 0 x = 0 ˙
61 60 ad2antll N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y x X N x = 0 x = 0 ˙
62 fveq2 x = a N x = N a
63 62 eqeq1d x = a N x = 0 N a = 0
64 eqeq1 x = a x = 0 ˙ a = 0 ˙
65 63 64 bibi12d x = a N x = 0 x = 0 ˙ N a = 0 a = 0 ˙
66 65 rspccva x X N x = 0 x = 0 ˙ a X N a = 0 a = 0 ˙
67 61 66 sylan N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y a X N a = 0 a = 0 ˙
68 simpr N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y y X N x - ˙ y N x + N y
69 68 ralimi x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y x X y X N x - ˙ y N x + N y
70 69 ad2antll N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y x X y X N x - ˙ y N x + N y
71 fvoveq1 x = a N x - ˙ y = N a - ˙ y
72 62 oveq1d x = a N x + N y = N a + N y
73 71 72 breq12d x = a N x - ˙ y N x + N y N a - ˙ y N a + N y
74 oveq2 y = b a - ˙ y = a - ˙ b
75 74 fveq2d y = b N a - ˙ y = N a - ˙ b
76 fveq2 y = b N y = N b
77 76 oveq2d y = b N a + N y = N a + N b
78 75 77 breq12d y = b N a - ˙ y N a + N y N a - ˙ b N a + N b
79 73 78 rspc2va a X b X x X y X N x - ˙ y N x + N y N a - ˙ b N a + N b
80 79 ancoms x X y X N x - ˙ y N x + N y a X b X N a - ˙ b N a + N b
81 70 80 sylan N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y a X b X N a - ˙ b N a + N b
82 1 2 3 4 57 58 67 81 tngngpd N : X G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y T NrmGrp
83 56 82 impbida N : X T NrmGrp G Grp x X N x = 0 x = 0 ˙ y X N x - ˙ y N x + N y