Metamath Proof Explorer

Theorem norm1

Description: From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion norm1 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1

Proof

Step Hyp Ref Expression
1 normcl ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ
2 1 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℝ
3 normne0 ⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ
4 3 biimpar ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ≠ 0
5 2 4 rereccld ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℝ
6 5 recnd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℂ
7 simpl ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ ℋ
8 norm-iii ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A
9 6 7 8 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A
10 normgt0 ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A
11 10 biimpa ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < norm ℎ ⁡ A
12 1re ⊢ 1 ∈ ℝ
13 0le1 ⊢ 0 ≤ 1
14 divge0 ⊢ 1 ∈ ℝ ∧ 0 ≤ 1 ∧ norm ℎ ⁡ A ∈ ℝ ∧ 0 < norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
15 12 13 14 mpanl12 ⊢ norm ℎ ⁡ A ∈ ℝ ∧ 0 < norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
16 2 11 15 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A
17 5 16 absidd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A = 1 norm ℎ ⁡ A
18 17 oveq1d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A
19 1 recnd ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℂ
20 19 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℂ
21 20 4 recid2d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ A = 1
22 9 18 21 3eqtrd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1