Definition df-hba 24322

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 24352). 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 24520. (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 24272	. 2 class ~H
2		cva 24273	. . . . 5 class +h
3		csm 24274	. . . . 5 class .h
4	2, 3	cop 3878	. . . 4 class <. +h , .h >.
5		cno 24276	. . . 4 class normh
6	4, 5	cop 3878	. . 3 class <. <. +h , .h >. , normh >.
7		cba 23915	. . 3 class BaseSet
8	6, 7	cfv 5413	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1369	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  24334  axhfvadd-zf  24335  axhvcom-zf  24336  axhvass-zf  24337  axhv0cl-zf  24338  axhvaddid-zf  24339  axhfvmul-zf  24340  axhvmulid-zf  24341  axhvmulass-zf  24342  axhvdistr1-zf  24343  axhvdistr2-zf  24344  axhvmul0-zf  24345  axhfi-zf  24346  axhis1-zf  24347  axhis2-zf  24348  axhis3-zf  24349  axhis4-zf  24350  axhcompl-zf  24351  bcsiHIL  24533  hlimadd  24546  hhssabloi  24614  pjhthlem2  24746  nmopsetretHIL  25219  nmopub2tHIL  25265  hmopbdoptHIL  25343