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 )