Definition df-hba 26087

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 26117). 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 26285. (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 26037	. 2 class ~H
2		cva 26038	. . . . 5 class +h
3		csm 26039	. . . . 5 class .h
4	2, 3	cop 4022	. . . 4 class <. +h , .h >.
5		cno 26041	. . . 4 class normh
6	4, 5	cop 4022	. . 3 class <. <. +h , .h >. , normh >.
7		cba 25680	. . 3 class BaseSet
8	6, 7	cfv 5570	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1398	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  26099  axhfvadd-zf  26100  axhvcom-zf  26101  axhvass-zf  26102  axhv0cl-zf  26103  axhvaddid-zf  26104  axhfvmul-zf  26105  axhvmulid-zf  26106  axhvmulass-zf  26107  axhvdistr1-zf  26108  axhvdistr2-zf  26109  axhvmul0-zf  26110  axhfi-zf  26111  axhis1-zf  26112  axhis2-zf  26113  axhis3-zf  26114  axhis4-zf  26115  axhcompl-zf  26116  bcsiHIL  26298  hlimadd  26311  hhssabloi  26379  pjhthlem2  26511  nmopsetretHIL  26984  nmopub2tHIL  27030  hmopbdoptHIL  27108