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

Metamath Proof Explorer

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 = + ℎ ⋅ ℎ norm ℎ
Assertion hhhl ⊢ U ∈ CHil OLD

Proof

Step Hyp Ref Expression
1 hhhl.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 1 hhnv ⊢ U ∈ NrmCVec
3 eqid ⊢ IndMet ⁡ U = IndMet ⁡ U
4 1 3 hhcms ⊢ IndMet ⁡ U ∈ CMet ⁡ ℋ
5 1 hhba ⊢ ℋ = BaseSet ⁡ U
6 5 3 iscbn ⊢ U ∈ CBan ↔ U ∈ NrmCVec ∧ IndMet ⁡ U ∈ CMet ⁡ ℋ
7 2 4 6 mpbir2an ⊢ U ∈ CBan
8 1 hhph ⊢ U ∈ CPreHil OLD
9 ishlo ⊢ U ∈ CHil OLD ↔ U ∈ CBan ∧ U ∈ CPreHil OLD
10 7 8 9 mpbir2an ⊢ U ∈ CHil OLD