Description: The base set of Hilbert space. This theorem provides an independent proof of df-hba (see comments in that definition). (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | hhnv.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| Assertion | hhba | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hhnv.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| 2 | hilablo | ⊢ +ℎ ∈ AbelOp | |
| 3 | ablogrpo | ⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp ) | |
| 4 | 2 3 | ax-mp | ⊢ +ℎ ∈ GrpOp |
| 5 | ax-hfvadd | ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ | |
| 6 | 5 | fdmi | ⊢ dom +ℎ = ( ℋ × ℋ ) |
| 7 | 4 6 | grporn | ⊢ ℋ = ran +ℎ |
| 8 | eqid | ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 ) | |
| 9 | 1 | hhva | ⊢ +ℎ = ( +𝑣 ‘ 𝑈 ) |
| 10 | 8 9 | bafval | ⊢ ( BaseSet ‘ 𝑈 ) = ran +ℎ |
| 11 | 7 10 | eqtr4i | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) |