Metamath Proof Explorer

Theorem cphass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. See ipass , his5 . (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 cphass 
|- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., 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 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
7 eqid 
 |-  ( .r ` F ) = ( .r ` F )
8 3 1 2 4 5 7 ipass 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A ( .r ` F ) ( B ., C ) ) )
9 6 8 sylan 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A ( .r ` F ) ( B ., C ) ) )
10 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
11 3 clmmul 
 |-  ( W e. CMod -> x. = ( .r ` F ) )
12 10 11 syl 
 |-  ( W e. CPreHil -> x. = ( .r ` F ) )
13 12 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> x. = ( .r ` F ) )
14 13 oveqd 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( A x. ( B ., C ) ) = ( A ( .r ` F ) ( B ., C ) ) )
15 9 14 eqtr4d 
 |-  ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A x. ( B ., C ) ) )