Theorem hilvc

Description: Hilbert space is a complex vector space. Vector addition is +h , and scalar product is .h . (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	hilvc	⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD

Proof

Step	Hyp	Ref	Expression
1		hilablo	⊢ +ℎ ∈ AbelOp
2		ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
3	2	fdmi	⊢ dom +ℎ = ( ℋ × ℋ )
4		ax-hfvmul	⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ
5		ax-hvmulid	⊢ ( 𝑥 ∈ ℋ → ( 1 ·ℎ 𝑥 ) = 𝑥 )
6		ax-hvdistr1	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑦 ·ℎ 𝑧 ) ) )
7		ax-hvdistr2	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 + 𝑧 ) ·ℎ 𝑥 ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑧 ·ℎ 𝑥 ) ) )
8		ax-hvmulass	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 · 𝑧 ) ·ℎ 𝑥 ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) )
9		eqid	⊢ ⟨ +ℎ , ·ℎ ⟩ = ⟨ +ℎ , ·ℎ ⟩
10	1 3 4 5 6 7 8 9	isvciOLD	⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD