Description: Derive Axiom ax-hfi from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | axhil.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| axhil.2 | ⊢ 𝑈 ∈ CHilOLD | ||
| axhfi.1 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | ||
| Assertion | axhfi-zf | ⊢ ·ih : ( ℋ × ℋ ) ⟶ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axhil.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| 2 | axhil.2 | ⊢ 𝑈 ∈ CHilOLD | |
| 3 | axhfi.1 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | |
| 4 | df-hba | ⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) | |
| 5 | 1 | fveq2i | ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
| 6 | 4 5 | eqtr4i | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) |
| 7 | 6 3 | hlipf | ⊢ ( 𝑈 ∈ CHilOLD → ·ih : ( ℋ × ℋ ) ⟶ ℂ ) |
| 8 | 2 7 | ax-mp | ⊢ ·ih : ( ℋ × ℋ ) ⟶ ℂ |