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}_{\mathrm{OLD}}$$

Proof

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