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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 )

Proof

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