Step |
Hyp |
Ref |
Expression |
1 |
|
cnnv.6 |
|- U = <. <. + , x. >. , abs >. |
2 |
|
cnaddabloOLD |
|- + e. AbelOp |
3 |
|
ablogrpo |
|- ( + e. AbelOp -> + e. GrpOp ) |
4 |
2 3
|
ax-mp |
|- + e. GrpOp |
5 |
|
ax-addf |
|- + : ( CC X. CC ) --> CC |
6 |
5
|
fdmi |
|- dom + = ( CC X. CC ) |
7 |
4 6
|
grporn |
|- CC = ran + |
8 |
|
cnidOLD |
|- 0 = ( GId ` + ) |
9 |
|
cncvcOLD |
|- <. + , x. >. e. CVecOLD |
10 |
|
absf |
|- abs : CC --> RR |
11 |
|
abs00 |
|- ( x e. CC -> ( ( abs ` x ) = 0 <-> x = 0 ) ) |
12 |
11
|
biimpa |
|- ( ( x e. CC /\ ( abs ` x ) = 0 ) -> x = 0 ) |
13 |
|
absmul |
|- ( ( y e. CC /\ x e. CC ) -> ( abs ` ( y x. x ) ) = ( ( abs ` y ) x. ( abs ` x ) ) ) |
14 |
|
abstri |
|- ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x + y ) ) <_ ( ( abs ` x ) + ( abs ` y ) ) ) |
15 |
7 8 9 10 12 13 14 1
|
isnvi |
|- U e. NrmCVec |