Step |
Hyp |
Ref |
Expression |
1 |
|
isnvi.5 |
|- X = ran G |
2 |
|
isnvi.6 |
|- Z = ( GId ` G ) |
3 |
|
isnvi.7 |
|- <. G , S >. e. CVecOLD |
4 |
|
isnvi.8 |
|- N : X --> RR |
5 |
|
isnvi.9 |
|- ( ( x e. X /\ ( N ` x ) = 0 ) -> x = Z ) |
6 |
|
isnvi.10 |
|- ( ( y e. CC /\ x e. X ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) ) |
7 |
|
isnvi.11 |
|- ( ( x e. X /\ y e. X ) -> ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) |
8 |
|
isnvi.12 |
|- U = <. <. G , S >. , N >. |
9 |
5
|
ex |
|- ( x e. X -> ( ( N ` x ) = 0 -> x = Z ) ) |
10 |
6
|
ancoms |
|- ( ( x e. X /\ y e. CC ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) ) |
11 |
10
|
ralrimiva |
|- ( x e. X -> A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) ) |
12 |
7
|
ralrimiva |
|- ( x e. X -> A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) |
13 |
9 11 12
|
3jca |
|- ( 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 ) ) ) ) |
14 |
13
|
rgen |
|- 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 ) ) ) |
15 |
1 2
|
isnv |
|- ( <. <. 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 ) ) ) ) ) |
16 |
3 4 14 15
|
mpbir3an |
|- <. <. G , S >. , N >. e. NrmCVec |
17 |
8 16
|
eqeltri |
|- U e. NrmCVec |