Definition df-hba 25562

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 25592). 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 25760. (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 25512	. 2 class ~H
2		cva 25513	. . . . 5 class +h
3		csm 25514	. . . . 5 class .h
4	2, 3	cop 4033	. . . 4 class <. +h , .h >.
5		cno 25516	. . . 4 class normh
6	4, 5	cop 4033	. . 3 class <. <. +h , .h >. , normh >.
7		cba 25155	. . 3 class BaseSet
8	6, 7	cfv 5586	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1379	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  25574  axhfvadd-zf  25575  axhvcom-zf  25576  axhvass-zf  25577  axhv0cl-zf  25578  axhvaddid-zf  25579  axhfvmul-zf  25580  axhvmulid-zf  25581  axhvmulass-zf  25582  axhvdistr1-zf  25583  axhvdistr2-zf  25584  axhvmul0-zf  25585  axhfi-zf  25586  axhis1-zf  25587  axhis2-zf  25588  axhis3-zf  25589  axhis4-zf  25590  axhcompl-zf  25591  bcsiHIL  25773  hlimadd  25786  hhssabloi  25854  pjhthlem2  25986  nmopsetretHIL  26459  nmopub2tHIL  26505  hmopbdoptHIL  26583