Metamath Proof Explorer

Theorem cphassr

Description: "Associative" law for second argument of inner product (compare cphass ). See ipassr , his52 . (Contributed by Mario Carneiro, 16-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 cphassr 
|- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., ( A .x. C ) ) = ( ( * ` A ) x. ( B ., C ) ) )

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 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
7 6 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> W e. CMod )
8 3 clmmul 
 |-  ( W e. CMod -> x. = ( .r ` F ) )
9 7 8 syl 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> x. = ( .r ` F ) )
10 eqidd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., C ) = ( B ., C ) )
11 3 clmcj 
 |-  ( W e. CMod -> * = ( *r ` F ) )
12 7 11 syl 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> * = ( *r ` F ) )
13 12 fveq1d 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( * ` A ) = ( ( *r ` F ) ` A ) )
14 9 10 13 oveq123d 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( B ., C ) x. ( * ` A ) ) = ( ( B ., C ) ( .r ` F ) ( ( *r ` F ) ` A ) ) )
15 3 4 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
16 7 15 syl 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> K C_ CC )
17 simpr1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> A e. K )
18 16 17 sseldd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> A e. CC )
19 18 cjcld 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( * ` A ) e. CC )
20 2 1 cphipcl 
 |-  ( ( W e. CPreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. CC )
21 20 3adant3r1 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., C ) e. CC )
22 19 21 mulcomd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( * ` A ) x. ( B ., C ) ) = ( ( B ., C ) x. ( * ` A ) ) )
23 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
24 3anrot 
 |-  ( ( A e. K /\ B e. V /\ C e. V ) <-> ( B e. V /\ C e. V /\ A e. K ) )
25 24 biimpi 
 |-  ( ( A e. K /\ B e. V /\ C e. V ) -> ( B e. V /\ C e. V /\ A e. K ) )
26 eqid 
 |-  ( .r ` F ) = ( .r ` F )
27 eqid 
 |-  ( *r ` F ) = ( *r ` F )
28 3 1 2 4 5 26 27 ipassr 
 |-  ( ( W e. PreHil /\ ( B e. V /\ C e. V /\ A e. K ) ) -> ( B ., ( A .x. C ) ) = ( ( B ., C ) ( .r ` F ) ( ( *r ` F ) ` A ) ) )
29 23 25 28 syl2an 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., ( A .x. C ) ) = ( ( B ., C ) ( .r ` F ) ( ( *r ` F ) ` A ) ) )
30 14 22 29 3eqtr4rd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., ( A .x. C ) ) = ( ( * ` A ) x. ( B ., C ) ) )