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 )