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	$⊢ ⟨+_{ℎ}, \cdot_{ℎ}⟩ \in {CVec}_{OLD}$

Proof

Step	Hyp	Ref	Expression
1		hilablo	$⊢ +_{ℎ} \in AbelOp$
2		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
3	2	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
4		ax-hfvmul	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ$
5		ax-hvmulid	$⊢ x \in ℋ \to 1 \cdot_{ℎ} x = x$
6		ax-hvdistr1	$⊢ (y \in ℂ \land x \in ℋ \land z \in ℋ) \to y \cdot_{ℎ} (x +_{ℎ} z) = (y \cdot_{ℎ} x) +_{ℎ} (y \cdot_{ℎ} z)$
7		ax-hvdistr2	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℋ) \to (y + z) \cdot_{ℎ} x = (y \cdot_{ℎ} x) +_{ℎ} (z \cdot_{ℎ} x)$
8		ax-hvmulass	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℋ) \to y z \cdot_{ℎ} x = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
9		eqid	$⊢ ⟨+_{ℎ}, \cdot_{ℎ}⟩ = ⟨+_{ℎ}, \cdot_{ℎ}⟩$
10	1 3 4 5 6 7 8 9	isvciOLD	$⊢ ⟨+_{ℎ}, \cdot_{ℎ}⟩ \in {CVec}_{OLD}$