Step |
Hyp |
Ref |
Expression |
1 |
|
nv1.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nv1.4 |
|- S = ( .sOLD ` U ) |
3 |
|
nv1.5 |
|- Z = ( 0vec ` U ) |
4 |
|
nv1.6 |
|- N = ( normCV ` U ) |
5 |
|
simp1 |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> U e. NrmCVec ) |
6 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR ) |
7 |
6
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` A ) e. RR ) |
8 |
1 3 4
|
nvz |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = Z ) ) |
9 |
8
|
necon3bid |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> A =/= Z ) ) |
10 |
9
|
biimp3ar |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` A ) =/= 0 ) |
11 |
7 10
|
rereccld |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( 1 / ( N ` A ) ) e. RR ) |
12 |
1 3 4
|
nvgt0 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= Z <-> 0 < ( N ` A ) ) ) |
13 |
12
|
biimp3a |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> 0 < ( N ` A ) ) |
14 |
|
1re |
|- 1 e. RR |
15 |
|
0le1 |
|- 0 <_ 1 |
16 |
|
divge0 |
|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( N ` A ) e. RR /\ 0 < ( N ` A ) ) ) -> 0 <_ ( 1 / ( N ` A ) ) ) |
17 |
14 15 16
|
mpanl12 |
|- ( ( ( N ` A ) e. RR /\ 0 < ( N ` A ) ) -> 0 <_ ( 1 / ( N ` A ) ) ) |
18 |
7 13 17
|
syl2anc |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> 0 <_ ( 1 / ( N ` A ) ) ) |
19 |
|
simp2 |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> A e. X ) |
20 |
1 2 4
|
nvsge0 |
|- ( ( U e. NrmCVec /\ ( ( 1 / ( N ` A ) ) e. RR /\ 0 <_ ( 1 / ( N ` A ) ) ) /\ A e. X ) -> ( N ` ( ( 1 / ( N ` A ) ) S A ) ) = ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) ) |
21 |
5 11 18 19 20
|
syl121anc |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` ( ( 1 / ( N ` A ) ) S A ) ) = ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) ) |
22 |
6
|
recnd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. CC ) |
23 |
22
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` A ) e. CC ) |
24 |
23 10
|
recid2d |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( ( 1 / ( N ` A ) ) x. ( N ` A ) ) = 1 ) |
25 |
21 24
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` ( ( 1 / ( N ` A ) ) S A ) ) = 1 ) |