Metamath Proof Explorer

Theorem cphdi

Description: Distributive law for inner product (left-distributivity). Complex version of ipdi . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h 
|- ., = ( .i ` W )
cphipcj.v 
|- V = ( Base ` W )
cphdir.P 
|- .+ = ( +g ` W )
Assertion cphdi 
|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) + ( A ., C ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h 
 |-  ., = ( .i ` W )
2 cphipcj.v 
 |-  V = ( Base ` W )
3 cphdir.P 
 |-  .+ = ( +g ` W )
4 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
7 5 1 2 3 6 ipdi 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) ( +g ` ( Scalar ` W ) ) ( A ., C ) ) )
8 4 7 sylan 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) ( +g ` ( Scalar ` W ) ) ( A ., C ) ) )
9 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
10 5 clmadd 
 |-  ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
11 9 10 syl 
 |-  ( W e. CPreHil -> + = ( +g ` ( Scalar ` W ) ) )
12 11 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> + = ( +g ` ( Scalar ` W ) ) )
13 12 oveqd 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A ., B ) + ( A ., C ) ) = ( ( A ., B ) ( +g ` ( Scalar ` W ) ) ( A ., C ) ) )
14 8 13 eqtr4d 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) + ( A ., C ) ) )