Definition df-hba 26671

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 26701). 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 26869. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hba	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

Detailed syntax breakdown of Definition df-hba

Step	Hyp	Ref	Expression
1		chil 26621	. 2 class ~H
2		cva 26622	. . . . 5 class +h
3		csm 26623	. . . . 5 class .h
4	2, 3	cop 3986	. . . 4 class <. +h , .h >.
5		cno 26625	. . . 4 class normh
6	4, 5	cop 3986	. . 3 class <. <. +h , .h >. , normh >.
7		cba 26254	. . 3 class BaseSet
8	6, 7	cfv 5601	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1455	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  26683  axhfvadd-zf  26684  axhvcom-zf  26685  axhvass-zf  26686  axhv0cl-zf  26687  axhvaddid-zf  26688  axhfvmul-zf  26689  axhvmulid-zf  26690  axhvmulass-zf  26691  axhvdistr1-zf  26692  axhvdistr2-zf  26693  axhvmul0-zf  26694  axhfi-zf  26695  axhis1-zf  26696  axhis2-zf  26697  axhis3-zf  26698  axhis4-zf  26699  axhcompl-zf  26700  bcsiHIL  26882  hlimadd  26895  hhssabloi  26962  pjhthlem2  27094  nmopsetretHIL  27566  nmopub2tHIL  27612  hmopbdoptHIL  27690