Step |
Hyp |
Ref |
Expression |
1 |
|
nvz0.5 |
|- Z = ( 0vec ` U ) |
2 |
|
nvz0.6 |
|- N = ( normCV ` U ) |
3 |
|
eqid |
|- ( BaseSet ` U ) = ( BaseSet ` U ) |
4 |
3 1
|
nvzcl |
|- ( U e. NrmCVec -> Z e. ( BaseSet ` U ) ) |
5 |
|
0re |
|- 0 e. RR |
6 |
|
0le0 |
|- 0 <_ 0 |
7 |
5 6
|
pm3.2i |
|- ( 0 e. RR /\ 0 <_ 0 ) |
8 |
|
eqid |
|- ( .sOLD ` U ) = ( .sOLD ` U ) |
9 |
3 8 2
|
nvsge0 |
|- ( ( U e. NrmCVec /\ ( 0 e. RR /\ 0 <_ 0 ) /\ Z e. ( BaseSet ` U ) ) -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) ) |
10 |
7 9
|
mp3an2 |
|- ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) ) |
11 |
4 10
|
mpdan |
|- ( U e. NrmCVec -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) ) |
12 |
3 8 1
|
nv0 |
|- ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( 0 ( .sOLD ` U ) Z ) = Z ) |
13 |
4 12
|
mpdan |
|- ( U e. NrmCVec -> ( 0 ( .sOLD ` U ) Z ) = Z ) |
14 |
13
|
fveq2d |
|- ( U e. NrmCVec -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( N ` Z ) ) |
15 |
3 2
|
nvcl |
|- ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` Z ) e. RR ) |
16 |
15
|
recnd |
|- ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` Z ) e. CC ) |
17 |
4 16
|
mpdan |
|- ( U e. NrmCVec -> ( N ` Z ) e. CC ) |
18 |
17
|
mul02d |
|- ( U e. NrmCVec -> ( 0 x. ( N ` Z ) ) = 0 ) |
19 |
11 14 18
|
3eqtr3d |
|- ( U e. NrmCVec -> ( N ` Z ) = 0 ) |