Theorem hhnv

Description: Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hhnv	⊢ 𝑈 ∈ NrmCVec

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hilablo	⊢ +ℎ ∈ AbelOp
3		ablogrpo	⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp )
4	2 3	ax-mp	⊢ +ℎ ∈ GrpOp
5		ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
6	5	fdmi	⊢ dom +ℎ = ( ℋ × ℋ )
7	4 6	grporn	⊢ ℋ = ran +ℎ
8		hilid	⊢ ( GId ‘ +ℎ ) = 0ℎ
9	8	eqcomi	⊢ 0ℎ = ( GId ‘ +ℎ )
10		hilvc	⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD
11		normf	⊢ normℎ : ℋ ⟶ ℝ
12		norm-i	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
13	12	biimpa	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) = 0 ) → 𝑥 = 0ℎ )
14		norm-iii	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
15		norm-ii	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) )
16	7 9 10 11 13 14 15 1	isnvi	⊢ 𝑈 ∈ NrmCVec