Metamath Proof Explorer

Theorem isnvlem

Description: Lemma for isnv . (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isnvlem.1 
|- X = ran G
isnvlem.2 
|- Z = ( GId ` G )
Assertion isnvlem 
|- ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. G , S >. , N >. e. NrmCVec <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isnvlem.1 
 |-  X = ran G
2 isnvlem.2 
 |-  Z = ( GId ` G )
3 df-nv 
 |-  NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }
4 3 eleq2i 
 |-  ( <. <. G , S >. , N >. e. NrmCVec <-> <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) } )
5 opeq1 
 |-  ( g = G -> <. g , s >. = <. G , s >. )
6 5 eleq1d 
 |-  ( g = G -> ( <. g , s >. e. CVecOLD <-> <. G , s >. e. CVecOLD ) )
7 rneq 
 |-  ( g = G -> ran g = ran G )
8 7 1 eqtr4di 
 |-  ( g = G -> ran g = X )
9 8 feq2d 
 |-  ( g = G -> ( n : ran g --> RR <-> n : X --> RR ) )
10 fveq2 
 |-  ( g = G -> ( GId ` g ) = ( GId ` G ) )
11 10 2 eqtr4di 
 |-  ( g = G -> ( GId ` g ) = Z )
12 11 eqeq2d 
 |-  ( g = G -> ( x = ( GId ` g ) <-> x = Z ) )
13 12 imbi2d 
 |-  ( g = G -> ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) <-> ( ( n ` x ) = 0 -> x = Z ) ) )
14 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
15 14 fveq2d 
 |-  ( g = G -> ( n ` ( x g y ) ) = ( n ` ( x G y ) ) )
16 15 breq1d 
 |-  ( g = G -> ( ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) <-> ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) )
17 8 16 raleqbidv 
 |-  ( g = G -> ( A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) <-> A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) )
18 13 17 3anbi13d 
 |-  ( g = G -> ( ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) )
19 8 18 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) )
20 6 9 19 3anbi123d 
 |-  ( g = G -> ( ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) <-> ( <. G , s >. e. CVecOLD /\ n : X --> RR /\ A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) )
21 opeq2 
 |-  ( s = S -> <. G , s >. = <. G , S >. )
22 21 eleq1d 
 |-  ( s = S -> ( <. G , s >. e. CVecOLD <-> <. G , S >. e. CVecOLD ) )
23 oveq 
 |-  ( s = S -> ( y s x ) = ( y S x ) )
24 23 fveqeq2d 
 |-  ( s = S -> ( ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) <-> ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) ) )
25 24 ralbidv 
 |-  ( s = S -> ( A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) <-> A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) ) )
26 25 3anbi2d 
 |-  ( s = S -> ( ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) )
27 26 ralbidv 
 |-  ( s = S -> ( A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) )
28 22 27 3anbi13d 
 |-  ( s = S -> ( ( <. G , s >. e. CVecOLD /\ n : X --> RR /\ A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) <-> ( <. G , S >. e. CVecOLD /\ n : X --> RR /\ A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) ) )
29 feq1 
 |-  ( n = N -> ( n : X --> RR <-> N : X --> RR ) )
30 fveq1 
 |-  ( n = N -> ( n ` x ) = ( N ` x ) )
31 30 eqeq1d 
 |-  ( n = N -> ( ( n ` x ) = 0 <-> ( N ` x ) = 0 ) )
32 31 imbi1d 
 |-  ( n = N -> ( ( ( n ` x ) = 0 -> x = Z ) <-> ( ( N ` x ) = 0 -> x = Z ) ) )
33 fveq1 
 |-  ( n = N -> ( n ` ( y S x ) ) = ( N ` ( y S x ) ) )
34 30 oveq2d 
 |-  ( n = N -> ( ( abs ` y ) x. ( n ` x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
35 33 34 eqeq12d 
 |-  ( n = N -> ( ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) <-> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) ) )
36 35 ralbidv 
 |-  ( n = N -> ( A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) <-> A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) ) )
37 fveq1 
 |-  ( n = N -> ( n ` ( x G y ) ) = ( N ` ( x G y ) ) )
38 fveq1 
 |-  ( n = N -> ( n ` y ) = ( N ` y ) )
39 30 38 oveq12d 
 |-  ( n = N -> ( ( n ` x ) + ( n ` y ) ) = ( ( N ` x ) + ( N ` y ) ) )
40 37 39 breq12d 
 |-  ( n = N -> ( ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) <-> ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
41 40 ralbidv 
 |-  ( n = N -> ( A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) <-> A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
42 32 36 41 3anbi123d 
 |-  ( n = N -> ( ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
43 42 ralbidv 
 |-  ( n = N -> ( A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) <-> A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
44 29 43 3anbi23d 
 |-  ( n = N -> ( ( <. G , S >. e. CVecOLD /\ n : X --> RR /\ A. x e. X ( ( ( n ` x ) = 0 -> x = Z ) /\ A. y e. CC ( n ` ( y S x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. X ( n ` ( x G y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
45 20 28 44 eloprabg 
 |-  ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) } <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
46 4 45 bitrid 
 |-  ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. G , S >. , N >. e. NrmCVec <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )