Theorem axhv0cl-zf

Description: Derive Axiom ax-hv0cl from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	axhil.1	|- U = <. <. +h , .h >. , normh >.
	axhil.2	|- U e. CHilOLD
Assertion	axhv0cl-zf	|- 0h e. ~H

Proof

Step	Hyp	Ref	Expression
1		axhil.1	|- U = <. <. +h , .h >. , normh >.
2		axhil.2	|- U e. CHilOLD
3		df-hba	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
4	1	fveq2i	|- ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. )
5	3 4	eqtr4i	|- ~H = ( BaseSet ` U )
6		df-h0v	|- 0h = ( 0vec ` <. <. +h , .h >. , normh >. )
7	1	fveq2i	|- ( 0vec ` U ) = ( 0vec ` <. <. +h , .h >. , normh >. )
8	6 7	eqtr4i	|- 0h = ( 0vec ` U )
9	5 8	hl0cl	|- ( U e. CHilOLD -> 0h e. ~H )
10	2 9	ax-mp	|- 0h e. ~H