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ℎ⁡1normℎ⁡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ℎ→1normℎ⁡A∈ℝ
6 5 recnd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A∈ℂ
7 simpl ⊢A∈ℋ∧A≠0ℎ→A∈ℋ
8 norm-iii ⊢1normℎ⁡A∈ℂ∧A∈ℋ→normℎ⁡1normℎ⁡A⋅ℎA=1normℎ⁡A⁢normℎ⁡A
9 6 7 8 syl2anc ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA=1normℎ⁡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≤1normℎ⁡A
15 12 13 14 mpanl12 ⊢normℎ⁡A∈ℝ∧0<normℎ⁡A→0≤1normℎ⁡A
16 2 11 15 syl2anc ⊢A∈ℋ∧A≠0ℎ→0≤1normℎ⁡A
17 5 16 absidd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A=1normℎ⁡A
18 17 oveq1d ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢normℎ⁡A=1normℎ⁡A⁢normℎ⁡A
19 1 recnd ⊢A∈ℋ→normℎ⁡A∈ℂ
20 19 adantr ⊢A∈ℋ∧A≠0ℎ→normℎ⁡A∈ℂ
21 20 4 recid2d ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢normℎ⁡A=1
22 9 18 21 3eqtrd ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA=1