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

Metamath Proof Explorer

Theorem hlobn

Description: Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	hlobn	$⊢ U \in {CHil}_{OLD} \to U \in CBan$

Step	Hyp	Ref	Expression
1		ishlo	$⊢ U \in {CHil}_{OLD} \leftrightarrow (U \in CBan \land U \in {CPreHil}_{OLD})$
2	1	simplbi	$⊢ U \in {CHil}_{OLD} \to U \in CBan$