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
|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chba
 |-  ~H
1 cba
 |-  BaseSet
2 cva
 |-  +h
3 csm
 |-  .h
4 2 3 cop
 |-  <. +h , .h >.
5 cno
 |-  normh
6 4 5 cop
 |-  <. <. +h , .h >. , normh >.
7 6 1 cfv
 |-  ( BaseSet ` <. <. +h , .h >. , normh >. )
8 0 7 wceq
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )