Theorem axhvdistr1-zf

Description: Derive Axiom ax-hvdistr1 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	axhvdistr1-zf	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) ) )

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	2	hlnvi	|- U e. NrmCVec
7	1 6	h2hva	|- +h = ( +v ` U )
8	1 6	h2hsm	|- .h = ( .sOLD ` U )
9	5 7 8	hldi	|- ( ( U e. CHilOLD /\ ( A e. CC /\ B e. ~H /\ C e. ~H ) ) -> ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) ) )
10	2 9	mpan	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) ) )