This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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