Theorem axhis4-zf

Description: Derive Axiom ax-his4 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
	axhfi.1	|- .ih = ( .iOLD ` U )
Assertion	axhis4-zf	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )

Proof

Step	Hyp	Ref	Expression
1		axhil.1	|- U = <. <. +h , .h >. , normh >.
2		axhil.2	|- U e. CHilOLD
3		axhfi.1	|- .ih = ( .iOLD ` U )
4		df-hba	|- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
5	1	fveq2i	|- ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. )
6	4 5	eqtr4i	|- ~H = ( BaseSet ` U )
7		df-h0v	|- 0h = ( 0vec ` <. <. +h , .h >. , normh >. )
8	1	fveq2i	|- ( 0vec ` U ) = ( 0vec ` <. <. +h , .h >. , normh >. )
9	7 8	eqtr4i	|- 0h = ( 0vec ` U )
10	6 9 3	hlipgt0	|- ( ( U e. CHilOLD /\ A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )
11	2 10	mp3an1	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( A .ih A ) )