Definition df-hba 22425

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 22455). 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 22622. (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 22375	. 2 class ~H
2		cva 22376	. . . . 5 class +h
3		csm 22377	. . . . 5 class .h
4	2, 3	cop 3777	. . . 4 class <. +h , .h >.
5		cno 22379	. . . 4 class normh
6	4, 5	cop 3777	. . 3 class <. <. +h , .h >. , normh >.
7		cba 22018	. . 3 class BaseSet
8	6, 7	cfv 5413	. 2 class ( BaseSet ` <. <. +h , .h >. , normh >. )
9	1, 8	wceq 1649	1 wff ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

This definition is referenced by:  axhilex-zf  22437  axhfvadd-zf  22438  axhvcom-zf  22439  axhvass-zf  22440  axhv0cl-zf  22441  axhvaddid-zf  22442  axhfvmul-zf  22443  axhvmulid-zf  22444  axhvmulass-zf  22445  axhvdistr1-zf  22446  axhvdistr2-zf  22447  axhvmul0-zf  22448  axhfi-zf  22449  axhis1-zf  22450  axhis2-zf  22451  axhis3-zf  22452  axhis4-zf  22453  axhcompl-zf  22454  bcsiHIL  22635  hlimadd  22648  hhssabloi  22715  pjhthlem2  22847  nmopsetretHIL  23320  nmopub2tHIL  23366  hmopbdoptHIL  23444