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 ` G )
tngngp.z 
|- .0. = ( 0g ` G )
Assertion tngngp 
|- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. 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 ` G )
4 tngngp.z 
 |-  .0. = ( 0g ` G )
5 eqid 
 |-  ( dist ` T ) = ( dist ` T )
6 1 2 5 tngngp2 
 |-  ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ ( dist ` T ) e. ( Met ` X ) ) ) )
7 6 simprbda 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> G e. Grp )
8 simplr 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> T e. NrmGrp )
9 simpr 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> x e. X )
10 2 fvexi 
 |-  X e. _V
11 reex 
 |-  RR e. _V
12 fex2 
 |-  ( ( N : X --> RR /\ X e. _V /\ RR e. _V ) -> N e. _V )
13 10 11 12 mp3an23 
 |-  ( N : X --> RR -> N e. _V )
14 13 ad2antrr 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> N e. _V )
15 1 2 tngbas 
 |-  ( N e. _V -> X = ( Base ` T ) )
16 14 15 syl 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> X = ( Base ` T ) )
17 9 16 eleqtrd 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> x e. ( Base ` T ) )
18 eqid 
 |-  ( Base ` T ) = ( Base ` T )
19 eqid 
 |-  ( norm ` T ) = ( norm ` T )
20 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
21 18 19 20 nmeq0 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) -> ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) )
22 8 17 21 syl2anc 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) )
23 7 adantr 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> G e. Grp )
24 simpll 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> N : X --> RR )
25 1 2 11 tngnm 
 |-  ( ( G e. Grp /\ N : X --> RR ) -> N = ( norm ` T ) )
26 23 24 25 syl2anc 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> N = ( norm ` T ) )
27 26 fveq1d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( N ` x ) = ( ( norm ` T ) ` x ) )
28 27 eqeq1d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( ( N ` x ) = 0 <-> ( ( norm ` T ) ` x ) = 0 ) )
29 1 4 tng0 
 |-  ( N e. _V -> .0. = ( 0g ` T ) )
30 14 29 syl 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> .0. = ( 0g ` T ) )
31 30 eqeq2d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( x = .0. <-> x = ( 0g ` T ) ) )
32 22 28 31 3bitr4d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
33 simpllr 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> T e. NrmGrp )
34 17 adantr 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> x e. ( Base ` T ) )
35 16 eleq2d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( y e. X <-> y e. ( Base ` T ) ) )
36 35 biimpa 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> y e. ( Base ` T ) )
37 eqid 
 |-  ( -g ` T ) = ( -g ` T )
38 18 19 37 nmmtri 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) /\ y e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( x ( -g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
39 33 34 36 38 syl3anc 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> ( ( norm ` T ) ` ( x ( -g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
40 2 16 eqtr3id 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( Base ` G ) = ( Base ` T ) )
41 eqid 
 |-  ( +g ` G ) = ( +g ` G )
42 1 41 tngplusg 
 |-  ( N e. _V -> ( +g ` G ) = ( +g ` T ) )
43 14 42 syl 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( +g ` G ) = ( +g ` T ) )
44 40 43 grpsubpropd 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( -g ` G ) = ( -g ` T ) )
45 3 44 eqtrid 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> .- = ( -g ` T ) )
46 45 oveqd 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( x .- y ) = ( x ( -g ` T ) y ) )
47 26 46 fveq12d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( N ` ( x .- y ) ) = ( ( norm ` T ) ` ( x ( -g ` T ) y ) ) )
48 47 adantr 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> ( N ` ( x .- y ) ) = ( ( norm ` T ) ` ( x ( -g ` T ) y ) ) )
49 26 fveq1d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( N ` y ) = ( ( norm ` T ) ` y ) )
50 27 49 oveq12d 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( ( N ` x ) + ( N ` y ) ) = ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
51 50 adantr 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> ( ( N ` x ) + ( N ` y ) ) = ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
52 39 48 51 3brtr4d 
 |-  ( ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) /\ y e. X ) -> ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
53 52 ralrimiva 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
54 32 53 jca 
 |-  ( ( ( N : X --> RR /\ T e. NrmGrp ) /\ x e. X ) -> ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
55 54 ralrimiva 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
56 7 55 jca 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
57 simprl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> G e. Grp )
58 simpl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> N : X --> RR )
59 simpl 
 |-  ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
60 59 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X ( ( N ` x ) = 0 <-> x = .0. ) )
61 60 ad2antll 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> A. x e. 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 
 |-  ( ( A. x e. X ( ( N ` x ) = 0 <-> x = .0. ) /\ a e. X ) -> ( ( N ` a ) = 0 <-> a = .0. ) )
67 61 66 sylan 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ a e. X ) -> ( ( N ` a ) = 0 <-> a = .0. ) )
68 simpr 
 |-  ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
69 68 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
70 69 ad2antll 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> A. x e. X A. y e. 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 e. X /\ b e. X ) /\ A. x e. X A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( N ` ( a .- b ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
80 79 ancoms 
 |-  ( ( A. x e. X A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .- b ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
81 70 80 sylan 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .- b ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
82 1 2 3 4 57 58 67 81 tngngpd 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> T e. NrmGrp )
83 56 82 impbida 
 |-  ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. X ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )