Definition df-hba 26457

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 26487). 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 26655. (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 26407	. 2 class ~H
2		cva 26408	. . . . 5 class +h
3		csm 26409	. . . . 5 class .h
4	2, 3	cop 4008	. . . 4 class <. +h , .h >.
5		cno 26411	. . . 4 class normh
6	4, 5	cop 4008	. . 3 class <. <. +h , .h >. , normh >.
7		cba 26050	. . 3 class BaseSet
8	6, 7	cfv 5601	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1437	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  26469  axhfvadd-zf  26470  axhvcom-zf  26471  axhvass-zf  26472  axhv0cl-zf  26473  axhvaddid-zf  26474  axhfvmul-zf  26475  axhvmulid-zf  26476  axhvmulass-zf  26477  axhvdistr1-zf  26478  axhvdistr2-zf  26479  axhvmul0-zf  26480  axhfi-zf  26481  axhis1-zf  26482  axhis2-zf  26483  axhis3-zf  26484  axhis4-zf  26485  axhcompl-zf  26486  bcsiHIL  26668  hlimadd  26681  hhssabloi  26748  pjhthlem2  26880  nmopsetretHIL  27352  nmopub2tHIL  27398  hmopbdoptHIL  27476