Theorem hhhl

Description: The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhhl.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
Assertion	hhhl	$$⊢U\in {CHil}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		hhhl.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
3		eqid	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{IndMet}\left(U\right)$$
4	1 3	hhcms	$$⊢\mathrm{IndMet}\left(U\right)\in \mathrm{CMet}\left(\mathscr{H}\right)$$
5	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
6	5 3	iscbn	$$⊢U\in \mathrm{CBan}\leftrightarrow \left(U\in \mathrm{NrmCVec}\wedge \mathrm{IndMet}\left(U\right)\in \mathrm{CMet}\left(\mathscr{H}\right)\right)$$
7	2 4 6	mpbir2an	$$⊢U\in \mathrm{CBan}$$
8	1	hhph	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
9		ishlo	$$⊢U\in {CHil}_{\mathrm{OLD}}\leftrightarrow \left(U\in \mathrm{CBan}\wedge U\in {CPreHil}_{\mathrm{OLD}}\right)$$
10	7 8 9	mpbir2an	$$⊢U\in {CHil}_{\mathrm{OLD}}$$