Theorem hlipdir

Description: Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlipdir.1	|- X = ( BaseSet ` U )
	hlipdir.2	|- G = ( +v ` U )
	hlipdir.7	|- P = ( .iOLD ` U )
Assertion	hlipdir	|- ( ( U e. CHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlipdir.1	|- X = ( BaseSet ` U )
2		hlipdir.2	|- G = ( +v ` U )
3		hlipdir.7	|- P = ( .iOLD ` U )
4		hlph	|- ( U e. CHilOLD -> U e. CPreHilOLD )
5	1 2 3	dipdir	|- ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) )
6	4 5	sylan	|- ( ( U e. CHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) )