Description: Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hilhh.1 | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) | |
| hilhh.2 | ⊢ +ℎ = ( +𝑣 ‘ 𝑈 ) | ||
| hilhh.3 | ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 ) | ||
| hilhh.5 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | ||
| hilhh.9 | ⊢ 𝑈 ∈ NrmCVec | ||
| Assertion | hilhhi | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hilhh.1 | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) | |
| 2 | hilhh.2 | ⊢ +ℎ = ( +𝑣 ‘ 𝑈 ) | |
| 3 | hilhh.3 | ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 ) | |
| 4 | hilhh.5 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | |
| 5 | hilhh.9 | ⊢ 𝑈 ∈ NrmCVec | |
| 6 | 1 4 5 | hilnormi | ⊢ normℎ = ( normCV ‘ 𝑈 ) |
| 7 | 2 3 6 | nvop | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
| 8 | 5 7 | ax-mp | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ |