Definition df-hba 27826

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 27856). 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 28024. (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 27776	. 2 class ~H
2		cva 27777	. . . . 5 class +h
3		csm 27778	. . . . 5 class .h
4	2, 3	cop 4183	. . . 4 class <. +h , .h >.
5		cno 27780	. . . 4 class normh
6	4, 5	cop 4183	. . 3 class <. <. +h , .h >. , normh >.
7		cba 27441	. . 3 class BaseSet
8	6, 7	cfv 5888	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1483	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  27838  axhfvadd-zf  27839  axhvcom-zf  27840  axhvass-zf  27841  axhv0cl-zf  27842  axhvaddid-zf  27843  axhfvmul-zf  27844  axhvmulid-zf  27845  axhvmulass-zf  27846  axhvdistr1-zf  27847  axhvdistr2-zf  27848  axhvmul0-zf  27849  axhfi-zf  27850  axhis1-zf  27851  axhis2-zf  27852  axhis3-zf  27853  axhis4-zf  27854  axhcompl-zf  27855  bcsiHIL  28037  hlimadd  28050  hhssabloilem  28118  pjhthlem2  28251  nmopsetretHIL  28723  nmopub2tHIL  28769  hmopbdoptHIL  28847