This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tngngp3

Description: Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021)

Ref Expression
Hypotheses tngngp3.t 
|- T = ( G toNrmGrp N )
tngngp3.x 
|- X = ( Base ` G )
tngngp3.z 
|- .0. = ( 0g ` G )
tngngp3.p 
|- .+ = ( +g ` G )
tngngp3.i 
|- I = ( invg ` G )
Assertion tngngp3 
|- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tngngp3.t 
 |-  T = ( G toNrmGrp N )
2 tngngp3.x 
 |-  X = ( Base ` G )
3 tngngp3.z 
 |-  .0. = ( 0g ` G )
4 tngngp3.p 
 |-  .+ = ( +g ` G )
5 tngngp3.i 
 |-  I = ( invg ` G )
6 2 fvexi 
 |-  X e. _V
7 fex 
 |-  ( ( N : X --> RR /\ X e. _V ) -> N e. _V )
8 6 7 mpan2 
 |-  ( N : X --> RR -> N e. _V )
9 1 tnggrpr 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> G e. Grp )
10 simp2 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> G e. Grp )
11 eqid 
 |-  ( Base ` T ) = ( Base ` T )
12 eqid 
 |-  ( norm ` T ) = ( norm ` T )
13 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
14 11 12 13 nmeq0 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) -> ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) )
15 eqid 
 |-  ( invg ` T ) = ( invg ` T )
16 11 12 15 nminv 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) )
17 eqid 
 |-  ( +g ` T ) = ( +g ` T )
18 11 12 17 nmtri 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) /\ y e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
19 18 3expa 
 |-  ( ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) /\ y e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
20 19 ralrimiva 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) -> A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
21 14 16 20 3jca 
 |-  ( ( T e. NrmGrp /\ x e. ( Base ` T ) ) -> ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
22 21 ralrimiva 
 |-  ( T e. NrmGrp -> A. x e. ( Base ` T ) ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
23 22 adantl 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> A. x e. ( Base ` T ) ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
24 23 3ad2ant1 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> A. x e. ( Base ` T ) ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
25 1 2 tngbas 
 |-  ( N e. _V -> X = ( Base ` T ) )
26 1 4 tngplusg 
 |-  ( N e. _V -> .+ = ( +g ` T ) )
27 eqidd 
 |-  ( N e. _V -> ( Base ` G ) = ( Base ` G ) )
28 eqid 
 |-  ( Base ` G ) = ( Base ` G )
29 1 28 tngbas 
 |-  ( N e. _V -> ( Base ` G ) = ( Base ` T ) )
30 eqid 
 |-  ( +g ` G ) = ( +g ` G )
31 1 30 tngplusg 
 |-  ( N e. _V -> ( +g ` G ) = ( +g ` T ) )
32 31 oveqd 
 |-  ( N e. _V -> ( x ( +g ` G ) y ) = ( x ( +g ` T ) y ) )
33 32 adantr 
 |-  ( ( N e. _V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` T ) y ) )
34 27 29 33 grpinvpropd 
 |-  ( N e. _V -> ( invg ` G ) = ( invg ` T ) )
35 5 34 eqtrid 
 |-  ( N e. _V -> I = ( invg ` T ) )
36 25 26 35 3jca 
 |-  ( N e. _V -> ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) )
37 36 adantr 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) )
38 37 3ad2ant1 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) )
39 reex 
 |-  RR e. _V
40 1 2 39 tngnm 
 |-  ( ( G e. Grp /\ N : X --> RR ) -> N = ( norm ` T ) )
41 40 3adant1 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> N = ( norm ` T ) )
42 1 3 tng0 
 |-  ( N e. _V -> .0. = ( 0g ` T ) )
43 42 adantr 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> .0. = ( 0g ` T ) )
44 43 3ad2ant1 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> .0. = ( 0g ` T ) )
45 38 41 44 3jca 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) )
46 simp1 
 |-  ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) -> X = ( Base ` T ) )
47 46 3ad2ant1 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> X = ( Base ` T ) )
48 simp2 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> N = ( norm ` T ) )
49 48 fveq1d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( N ` x ) = ( ( norm ` T ) ` x ) )
50 49 eqeq1d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( N ` x ) = 0 <-> ( ( norm ` T ) ` x ) = 0 ) )
51 simp3 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> .0. = ( 0g ` T ) )
52 51 eqeq2d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( x = .0. <-> x = ( 0g ` T ) ) )
53 50 52 bibi12d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( ( N ` x ) = 0 <-> x = .0. ) <-> ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) ) )
54 simp3 
 |-  ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) -> I = ( invg ` T ) )
55 54 3ad2ant1 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> I = ( invg ` T ) )
56 55 fveq1d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( I ` x ) = ( ( invg ` T ) ` x ) )
57 48 56 fveq12d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( N ` ( I ` x ) ) = ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) )
58 57 49 eqeq12d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( N ` ( I ` x ) ) = ( N ` x ) <-> ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) ) )
59 simp2 
 |-  ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) -> .+ = ( +g ` T ) )
60 59 3ad2ant1 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> .+ = ( +g ` T ) )
61 60 oveqd 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( x .+ y ) = ( x ( +g ` T ) y ) )
62 48 61 fveq12d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( N ` ( x .+ y ) ) = ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) )
63 fveq1 
 |-  ( N = ( norm ` T ) -> ( N ` x ) = ( ( norm ` T ) ` x ) )
64 fveq1 
 |-  ( N = ( norm ` T ) -> ( N ` y ) = ( ( norm ` T ) ` y ) )
65 63 64 oveq12d 
 |-  ( N = ( norm ` T ) -> ( ( N ` x ) + ( N ` y ) ) = ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
66 65 3ad2ant2 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( N ` x ) + ( N ` y ) ) = ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) )
67 62 66 breq12d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) <-> ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
68 47 67 raleqbidv 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) <-> A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) )
69 53 58 68 3anbi123d 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) ) )
70 47 69 raleqbidv 
 |-  ( ( ( X = ( Base ` T ) /\ .+ = ( +g ` T ) /\ I = ( invg ` T ) ) /\ N = ( norm ` T ) /\ .0. = ( 0g ` T ) ) -> ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> A. x e. ( Base ` T ) ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) ) )
71 45 70 syl 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> A. x e. ( Base ` T ) ( ( ( ( norm ` T ) ` x ) = 0 <-> x = ( 0g ` T ) ) /\ ( ( norm ` T ) ` ( ( invg ` T ) ` x ) ) = ( ( norm ` T ) ` x ) /\ A. y e. ( Base ` T ) ( ( norm ` T ) ` ( x ( +g ` T ) y ) ) <_ ( ( ( norm ` T ) ` x ) + ( ( norm ` T ) ` y ) ) ) ) )
72 24 71 mpbird 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
73 10 72 jca 
 |-  ( ( ( N e. _V /\ T e. NrmGrp ) /\ G e. Grp /\ N : X --> RR ) -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
74 73 3exp 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> ( G e. Grp -> ( N : X --> RR -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) ) )
75 9 74 mpd 
 |-  ( ( N e. _V /\ T e. NrmGrp ) -> ( N : X --> RR -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
76 75 expcom 
 |-  ( T e. NrmGrp -> ( N e. _V -> ( N : X --> RR -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) ) )
77 76 com13 
 |-  ( N : X --> RR -> ( N e. _V -> ( T e. NrmGrp -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) ) )
78 8 77 mpd 
 |-  ( N : X --> RR -> ( T e. NrmGrp -> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
79 eqid 
 |-  ( -g ` G ) = ( -g ` G )
80 simpl 
 |-  ( ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) -> G e. Grp )
81 80 adantl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> G e. Grp )
82 simpl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> N : X --> RR )
83 fveq2 
 |-  ( x = a -> ( N ` x ) = ( N ` a ) )
84 83 eqeq1d 
 |-  ( x = a -> ( ( N ` x ) = 0 <-> ( N ` a ) = 0 ) )
85 eqeq1 
 |-  ( x = a -> ( x = .0. <-> a = .0. ) )
86 84 85 bibi12d 
 |-  ( x = a -> ( ( ( N ` x ) = 0 <-> x = .0. ) <-> ( ( N ` a ) = 0 <-> a = .0. ) ) )
87 fveq2 
 |-  ( x = a -> ( I ` x ) = ( I ` a ) )
88 87 fveq2d 
 |-  ( x = a -> ( N ` ( I ` x ) ) = ( N ` ( I ` a ) ) )
89 88 83 eqeq12d 
 |-  ( x = a -> ( ( N ` ( I ` x ) ) = ( N ` x ) <-> ( N ` ( I ` a ) ) = ( N ` a ) ) )
90 fvoveq1 
 |-  ( x = a -> ( N ` ( x .+ y ) ) = ( N ` ( a .+ y ) ) )
91 83 oveq1d 
 |-  ( x = a -> ( ( N ` x ) + ( N ` y ) ) = ( ( N ` a ) + ( N ` y ) ) )
92 90 91 breq12d 
 |-  ( x = a -> ( ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) <-> ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) ) )
93 92 ralbidv 
 |-  ( x = a -> ( A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) <-> A. y e. X ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) ) )
94 86 89 93 3anbi123d 
 |-  ( x = a -> ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> ( ( ( N ` a ) = 0 <-> a = .0. ) /\ ( N ` ( I ` a ) ) = ( N ` a ) /\ A. y e. X ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) ) ) )
95 94 rspccva 
 |-  ( ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ a e. X ) -> ( ( ( N ` a ) = 0 <-> a = .0. ) /\ ( N ` ( I ` a ) ) = ( N ` a ) /\ A. y e. X ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) ) )
96 simp1 
 |-  ( ( ( ( N ` a ) = 0 <-> a = .0. ) /\ ( N ` ( I ` a ) ) = ( N ` a ) /\ A. y e. X ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) ) -> ( ( N ` a ) = 0 <-> a = .0. ) )
97 95 96 syl 
 |-  ( ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ a e. X ) -> ( ( N ` a ) = 0 <-> a = .0. ) )
98 97 ex 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( a e. X -> ( ( N ` a ) = 0 <-> a = .0. ) ) )
99 98 adantl 
 |-  ( ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) -> ( a e. X -> ( ( N ` a ) = 0 <-> a = .0. ) ) )
100 99 adantl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> ( a e. X -> ( ( N ` a ) = 0 <-> a = .0. ) ) )
101 100 imp 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ a e. X ) -> ( ( N ` a ) = 0 <-> a = .0. ) )
102 2 4 5 79 grpsubval 
 |-  ( ( a e. X /\ b e. X ) -> ( a ( -g ` G ) b ) = ( a .+ ( I ` b ) ) )
103 102 adantl 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( a ( -g ` G ) b ) = ( a .+ ( I ` b ) ) )
104 103 fveq2d 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a ( -g ` G ) b ) ) = ( N ` ( a .+ ( I ` b ) ) ) )
105 3simpc 
 |-  ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
106 105 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
107 simpr 
 |-  ( ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
108 107 ralimi 
 |-  ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ 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 ) ) )
109 oveq2 
 |-  ( y = ( I ` b ) -> ( a .+ y ) = ( a .+ ( I ` b ) ) )
110 109 fveq2d 
 |-  ( y = ( I ` b ) -> ( N ` ( a .+ y ) ) = ( N ` ( a .+ ( I ` b ) ) ) )
111 fveq2 
 |-  ( y = ( I ` b ) -> ( N ` y ) = ( N ` ( I ` b ) ) )
112 111 oveq2d 
 |-  ( y = ( I ` b ) -> ( ( N ` a ) + ( N ` y ) ) = ( ( N ` a ) + ( N ` ( I ` b ) ) ) )
113 110 112 breq12d 
 |-  ( y = ( I ` b ) -> ( ( N ` ( a .+ y ) ) <_ ( ( N ` a ) + ( N ` y ) ) <-> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) )
114 92 113 rspc2v 
 |-  ( ( a e. X /\ ( I ` b ) e. X ) -> ( A. x e. X A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) )
115 2 5 grpinvcl 
 |-  ( ( G e. Grp /\ b e. X ) -> ( I ` b ) e. X )
116 115 ex 
 |-  ( G e. Grp -> ( b e. X -> ( I ` b ) e. X ) )
117 116 anim2d 
 |-  ( G e. Grp -> ( ( a e. X /\ b e. X ) -> ( a e. X /\ ( I ` b ) e. X ) ) )
118 117 imp 
 |-  ( ( G e. Grp /\ ( a e. X /\ b e. X ) ) -> ( a e. X /\ ( I ` b ) e. X ) )
119 114 118 syl11 
 |-  ( A. x e. X A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) -> ( ( G e. Grp /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) )
120 119 expd 
 |-  ( A. x e. X A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) -> ( G e. Grp -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) ) )
121 108 120 syl 
 |-  ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( G e. Grp -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) ) )
122 121 imp 
 |-  ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) ) )
123 122 imp 
 |-  ( ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` ( I ` b ) ) ) )
124 simpl 
 |-  ( ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( N ` ( I ` x ) ) = ( N ` x ) )
125 124 ralimi 
 |-  ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X ( N ` ( I ` x ) ) = ( N ` x ) )
126 fveq2 
 |-  ( x = b -> ( I ` x ) = ( I ` b ) )
127 126 fveq2d 
 |-  ( x = b -> ( N ` ( I ` x ) ) = ( N ` ( I ` b ) ) )
128 fveq2 
 |-  ( x = b -> ( N ` x ) = ( N ` b ) )
129 127 128 eqeq12d 
 |-  ( x = b -> ( ( N ` ( I ` x ) ) = ( N ` x ) <-> ( N ` ( I ` b ) ) = ( N ` b ) ) )
130 129 rspccva 
 |-  ( ( A. x e. X ( N ` ( I ` x ) ) = ( N ` x ) /\ b e. X ) -> ( N ` ( I ` b ) ) = ( N ` b ) )
131 130 eqcomd 
 |-  ( ( A. x e. X ( N ` ( I ` x ) ) = ( N ` x ) /\ b e. X ) -> ( N ` b ) = ( N ` ( I ` b ) ) )
132 131 ex 
 |-  ( A. x e. X ( N ` ( I ` x ) ) = ( N ` x ) -> ( b e. X -> ( N ` b ) = ( N ` ( I ` b ) ) ) )
133 125 132 syl 
 |-  ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( b e. X -> ( N ` b ) = ( N ` ( I ` b ) ) ) )
134 133 adantr 
 |-  ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) -> ( b e. X -> ( N ` b ) = ( N ` ( I ` b ) ) ) )
135 134 adantld 
 |-  ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) -> ( ( a e. X /\ b e. X ) -> ( N ` b ) = ( N ` ( I ` b ) ) ) )
136 135 imp 
 |-  ( ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) /\ ( a e. X /\ b e. X ) ) -> ( N ` b ) = ( N ` ( I ` b ) ) )
137 136 oveq2d 
 |-  ( ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) /\ ( a e. X /\ b e. X ) ) -> ( ( N ` a ) + ( N ` b ) ) = ( ( N ` a ) + ( N ` ( I ` b ) ) ) )
138 123 137 breqtrrd 
 |-  ( ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
139 138 ex 
 |-  ( ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ G e. Grp ) -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) ) )
140 139 ex 
 |-  ( A. x e. X ( ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( G e. Grp -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) ) ) )
141 106 140 syl 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( G e. Grp -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) ) ) )
142 141 impcom 
 |-  ( ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) ) )
143 142 adantl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> ( ( a e. X /\ b e. X ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) ) )
144 143 imp 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a .+ ( I ` b ) ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
145 104 144 eqbrtrd 
 |-  ( ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( N ` ( a ( -g ` G ) b ) ) <_ ( ( N ` a ) + ( N ` b ) ) )
146 1 2 79 3 81 82 101 145 tngngpd 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) -> T e. NrmGrp )
147 146 ex 
 |-  ( N : X --> RR -> ( ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) -> T e. NrmGrp ) )
148 78 147 impbid 
 |-  ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ A. x e. X ( ( ( N ` x ) = 0 <-> x = .0. ) /\ ( N ` ( I ` x ) ) = ( N ` x ) /\ A. y e. X ( N ` ( x .+ y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )