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 = ⋅ 𝑠OLD ⁡ U
nv1.5 ⊢ Z = 0 vec ⁡ U
nv1.6 ⊢ N = norm CV ⁡ U
Assertion nv1 ⊢ U ∈ NrmCVec ∧ A ∈ 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 = ⋅ 𝑠OLD ⁡ U
3 nv1.5 ⊢ Z = 0 vec ⁡ U
4 nv1.6 ⊢ N = norm CV ⁡ U
5 simp1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → U ∈ NrmCVec
6 1 4 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
7 6 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → N ⁡ A ∈ ℝ
8 1 3 4 nvz ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = 0 ↔ A = Z
9 8 necon3bid ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ≠ 0 ↔ A ≠ Z
10 9 biimp3ar ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → N ⁡ A ≠ 0
11 7 10 rereccld ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → 1 N ⁡ A ∈ ℝ
12 1 3 4 nvgt0 ⊢ U ∈ NrmCVec ∧ A ∈ X → A ≠ Z ↔ 0 < N ⁡ A
13 12 biimp3a ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → 0 < N ⁡ A
14 1re ⊢ 1 ∈ ℝ
15 0le1 ⊢ 0 ≤ 1
16 divge0 ⊢ 1 ∈ ℝ ∧ 0 ≤ 1 ∧ N ⁡ A ∈ ℝ ∧ 0 < N ⁡ A → 0 ≤ 1 N ⁡ A
17 14 15 16 mpanl12 ⊢ N ⁡ A ∈ ℝ ∧ 0 < N ⁡ A → 0 ≤ 1 N ⁡ A
18 7 13 17 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → 0 ≤ 1 N ⁡ A
19 simp2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → A ∈ X
20 1 2 4 nvsge0 ⊢ U ∈ NrmCVec ∧ 1 N ⁡ A ∈ ℝ ∧ 0 ≤ 1 N ⁡ A ∧ A ∈ X → N ⁡ 1 N ⁡ A S A = 1 N ⁡ A ⁢ N ⁡ A
21 5 11 18 19 20 syl121anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → N ⁡ 1 N ⁡ A S A = 1 N ⁡ A ⁢ N ⁡ A
22 6 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℂ
23 22 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → N ⁡ A ∈ ℂ
24 23 10 recid2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → 1 N ⁡ A ⁢ N ⁡ A = 1
25 21 24 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ A ≠ Z → N ⁡ 1 N ⁡ A S A = 1