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 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| Assertion | hhhl | ⊢ 𝑈 ∈ CHilOLD |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hhhl.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| 2 | 1 | hhnv | ⊢ 𝑈 ∈ NrmCVec |
| 3 | eqid | ⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 ) | |
| 4 | 1 3 | hhcms | ⊢ ( IndMet ‘ 𝑈 ) ∈ ( CMet ‘ ℋ ) |
| 5 | 1 | hhba | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) |
| 6 | 5 3 | iscbn | ⊢ ( 𝑈 ∈ CBan ↔ ( 𝑈 ∈ NrmCVec ∧ ( IndMet ‘ 𝑈 ) ∈ ( CMet ‘ ℋ ) ) ) |
| 7 | 2 4 6 | mpbir2an | ⊢ 𝑈 ∈ CBan |
| 8 | 1 | hhph | ⊢ 𝑈 ∈ CPreHilOLD |
| 9 | ishlo | ⊢ ( 𝑈 ∈ CHilOLD ↔ ( 𝑈 ∈ CBan ∧ 𝑈 ∈ CPreHilOLD ) ) | |
| 10 | 7 8 9 | mpbir2an | ⊢ 𝑈 ∈ CHilOLD |