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 𝑋 = ( BaseSet ‘ 𝑈 )
nv1.4 𝑆 = ( ·𝑠OLD𝑈 )
nv1.5 𝑍 = ( 0vec𝑈 )
nv1.6 𝑁 = ( normCV𝑈 )
Assertion nv1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁𝐴 ) ) 𝑆 𝐴 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 nv1.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nv1.4 𝑆 = ( ·𝑠OLD𝑈 )
3 nv1.5 𝑍 = ( 0vec𝑈 )
4 nv1.6 𝑁 = ( normCV𝑈 )
5 simp1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → 𝑈 ∈ NrmCVec )
6 1 4 nvcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) ∈ ℝ )
7 6 3adant3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁𝐴 ) ∈ ℝ )
8 1 3 4 nvz ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) = 0 ↔ 𝐴 = 𝑍 ) )
9 8 necon3bid ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( ( 𝑁𝐴 ) ≠ 0 ↔ 𝐴𝑍 ) )
10 9 biimp3ar ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁𝐴 ) ≠ 0 )
11 7 10 rereccld ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 1 / ( 𝑁𝐴 ) ) ∈ ℝ )
12 1 3 4 nvgt0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝐴𝑍 ↔ 0 < ( 𝑁𝐴 ) ) )
13 12 biimp3a ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → 0 < ( 𝑁𝐴 ) )
14 1re 1 ∈ ℝ
15 0le1 0 ≤ 1
16 divge0 ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( 𝑁𝐴 ) ∈ ℝ ∧ 0 < ( 𝑁𝐴 ) ) ) → 0 ≤ ( 1 / ( 𝑁𝐴 ) ) )
17 14 15 16 mpanl12 ( ( ( 𝑁𝐴 ) ∈ ℝ ∧ 0 < ( 𝑁𝐴 ) ) → 0 ≤ ( 1 / ( 𝑁𝐴 ) ) )
18 7 13 17 syl2anc ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → 0 ≤ ( 1 / ( 𝑁𝐴 ) ) )
19 simp2 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → 𝐴𝑋 )
20 1 2 4 nvsge0 ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / ( 𝑁𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝑁𝐴 ) ) ) ∧ 𝐴𝑋 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁𝐴 ) ) 𝑆 𝐴 ) ) = ( ( 1 / ( 𝑁𝐴 ) ) · ( 𝑁𝐴 ) ) )
21 5 11 18 19 20 syl121anc ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁𝐴 ) ) 𝑆 𝐴 ) ) = ( ( 1 / ( 𝑁𝐴 ) ) · ( 𝑁𝐴 ) ) )
22 6 recnd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) ∈ ℂ )
23 22 3adant3 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁𝐴 ) ∈ ℂ )
24 23 10 recid2d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( ( 1 / ( 𝑁𝐴 ) ) · ( 𝑁𝐴 ) ) = 1 )
25 21 24 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐴𝑍 ) → ( 𝑁 ‘ ( ( 1 / ( 𝑁𝐴 ) ) 𝑆 𝐴 ) ) = 1 )