Definition df-hba 24524

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 24554). 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 24722. (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 24474	. 2 class ~H
2		cva 24475	. . . . 5 class +h
3		csm 24476	. . . . 5 class .h
4	2, 3	cop 3992	. . . 4 class <. +h , .h >.
5		cno 24478	. . . 4 class normh
6	4, 5	cop 3992	. . 3 class <. <. +h , .h >. , normh >.
7		cba 24117	. . 3 class BaseSet
8	6, 7	cfv 5527	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1370	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  24536  axhfvadd-zf  24537  axhvcom-zf  24538  axhvass-zf  24539  axhv0cl-zf  24540  axhvaddid-zf  24541  axhfvmul-zf  24542  axhvmulid-zf  24543  axhvmulass-zf  24544  axhvdistr1-zf  24545  axhvdistr2-zf  24546  axhvmul0-zf  24547  axhfi-zf  24548  axhis1-zf  24549  axhis2-zf  24550  axhis3-zf  24551  axhis4-zf  24552  axhcompl-zf  24553  bcsiHIL  24735  hlimadd  24748  hhssabloi  24816  pjhthlem2  24948  nmopsetretHIL  25421  nmopub2tHIL  25467  hmopbdoptHIL  25545