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

Metamath Proof Explorer

Theorem cnchl

Description: The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	cnhl.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
	Assertion	cnchl	$⊢ U \in {CHil}_{OLD}$

Step	Hyp	Ref	Expression
1		cnhl.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2	1	cnbn	$⊢ U \in CBan$
3	1	cncph	$⊢ U \in {CPreHil}_{OLD}$
4		ishlo	$⊢ U \in {CHil}_{OLD} \leftrightarrow (U \in CBan \land U \in {CPreHil}_{OLD})$
5	2 3 4	mpbir2an	$⊢ U \in {CHil}_{OLD}$