Theorem hhba

Description: The base set of Hilbert space. This theorem provides an independent proof of df-hba (see comments in that definition). (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	|- U = <. <. +h , .h >. , normh >.
Assertion	hhba	|- ~H = ( BaseSet ` U )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	|- U = <. <. +h , .h >. , normh >.
2		hilablo	|- +h e. AbelOp
3		ablogrpo	|- ( +h e. AbelOp -> +h e. GrpOp )
4	2 3	ax-mp	|- +h e. GrpOp
5		ax-hfvadd	|- +h : ( ~H X. ~H ) --> ~H
6	5	fdmi	|- dom +h = ( ~H X. ~H )
7	4 6	grporn	|- ~H = ran +h
8		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
9	1	hhva	|- +h = ( +v ` U )
10	8 9	bafval	|- ( BaseSet ` U ) = ran +h
11	7 10	eqtr4i	|- ~H = ( BaseSet ` U )