Definition df-hba

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 ). 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 . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hba	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chba	|- ~H
1		cba	|- BaseSet
2		cva	|- +h
3		csm	|- .h
4	2 3	cop	|- <. +h , .h >.
5		cno	|- normh
6	4 5	cop	|- <. <. +h , .h >. , normh >.
7	6 1	cfv	|- ( BaseSet ` <. <. +h , .h >. , normh >. )
8	0 7	wceq	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )