Metamath Proof Explorer

Theorem cph2ass

Description: Move scalar multiplication to outside of inner product. See his35 . (Contributed by Mario Carneiro, 17-Oct-2015)

Ref Expression
Hypotheses cphipcj.h 
|- ., = ( .i ` W )
cphipcj.v 
|- V = ( Base ` W )
cphass.f 
|- F = ( Scalar ` W )
cphass.k 
|- K = ( Base ` F )
cphass.s 
|- .x. = ( .s ` W )
Assertion cph2ass 
|- ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( ( A x. ( * ` B ) ) x. ( C ., D ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h 
 |-  ., = ( .i ` W )
2 cphipcj.v 
 |-  V = ( Base ` W )
3 cphass.f 
 |-  F = ( Scalar ` W )
4 cphass.k 
 |-  K = ( Base ` F )
5 cphass.s 
 |-  .x. = ( .s ` W )
6 simp1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> W e. CPreHil )
7 simp2r 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> B e. K )
8 simp3l 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> C e. V )
9 simp3r 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> D e. V )
10 1 2 3 4 5 cphassr 
 |-  ( ( W e. CPreHil /\ ( B e. K /\ C e. V /\ D e. V ) ) -> ( C ., ( B .x. D ) ) = ( ( * ` B ) x. ( C ., D ) ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( C ., ( B .x. D ) ) = ( ( * ` B ) x. ( C ., D ) ) )
12 11 oveq2d 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( A x. ( C ., ( B .x. D ) ) ) = ( A x. ( ( * ` B ) x. ( C ., D ) ) ) )
13 simp2l 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> A e. K )
14 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
15 14 3ad2ant1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> W e. LMod )
16 2 3 5 4 lmodvscl 
 |-  ( ( W e. LMod /\ B e. K /\ D e. V ) -> ( B .x. D ) e. V )
17 15 7 9 16 syl3anc 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( B .x. D ) e. V )
18 1 2 3 4 5 cphass 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ C e. V /\ ( B .x. D ) e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( A x. ( C ., ( B .x. D ) ) ) )
19 6 13 8 17 18 syl13anc 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( A x. ( C ., ( B .x. D ) ) ) )
20 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
21 20 3ad2ant1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> W e. CMod )
22 3 4 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
23 21 22 syl 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> K C_ CC )
24 23 13 sseldd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> A e. CC )
25 23 7 sseldd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> B e. CC )
26 25 cjcld 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( * ` B ) e. CC )
27 2 1 cphipcl 
 |-  ( ( W e. CPreHil /\ C e. V /\ D e. V ) -> ( C ., D ) e. CC )
28 27 3expb 
 |-  ( ( W e. CPreHil /\ ( C e. V /\ D e. V ) ) -> ( C ., D ) e. CC )
29 28 3adant2 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( C ., D ) e. CC )
30 24 26 29 mulassd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A x. ( * ` B ) ) x. ( C ., D ) ) = ( A x. ( ( * ` B ) x. ( C ., D ) ) ) )
31 12 19 30 3eqtr4d 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( ( A x. ( * ` B ) ) x. ( C ., D ) ) )