Metamath Proof Explorer


Definition df-hba

Description: Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex ). Note that ~H is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as Theorem hhba . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hba ℋ = ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chba
1 cba BaseSet
2 cva +
3 csm ·
4 2 3 cop ⟨ + , ·
5 cno norm
6 4 5 cop ⟨ ⟨ + , · ⟩ , norm
7 6 1 cfv ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
8 0 7 wceq ℋ = ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )