Metamath Proof Explorer


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 ) ) )