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 class
1 cba class BaseSet
2 cva class +
3 csm class
4 2 3 cop class +
5 cno class norm
6 4 5 cop class + norm
7 6 1 cfv class BaseSet + norm
8 0 7 wceq wff = BaseSet + norm