Metamath Proof Explorer

Theorem nv1

Description: From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nv1.1 
|- X = ( BaseSet ` U )
nv1.4 
|- S = ( .sOLD ` U )
nv1.5 
|- Z = ( 0vec ` U )
nv1.6 
|- N = ( normCV ` U )
Assertion nv1 
|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( N ` ( ( 1 / ( N ` A ) ) S A ) ) = 1 )

Proof

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 )