Definition df-hba 24194

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 24224). 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 24392. (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 24144	. 2 class ~H
2		cva 24145	. . . . 5 class +h
3		csm 24146	. . . . 5 class .h
4	2, 3	cop 3871	. . . 4 class <. +h , .h >.
5		cno 24148	. . . 4 class normh
6	4, 5	cop 3871	. . 3 class <. <. +h , .h >. , normh >.
7		cba 23787	. . 3 class BaseSet
8	6, 7	cfv 5406	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1362	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  24206  axhfvadd-zf  24207  axhvcom-zf  24208  axhvass-zf  24209  axhv0cl-zf  24210  axhvaddid-zf  24211  axhfvmul-zf  24212  axhvmulid-zf  24213  axhvmulass-zf  24214  axhvdistr1-zf  24215  axhvdistr2-zf  24216  axhvmul0-zf  24217  axhfi-zf  24218  axhis1-zf  24219  axhis2-zf  24220  axhis3-zf  24221  axhis4-zf  24222  axhcompl-zf  24223  bcsiHIL  24405  hlimadd  24418  hhssabloi  24486  pjhthlem2  24618  nmopsetretHIL  25091  nmopub2tHIL  25137  hmopbdoptHIL  25215