This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipassr

Description: "Associative" law for second argument of inner product (compare ipass ). (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ipdir.f 
|- K = ( Base ` F )
ipass.s 
|- .x. = ( .s ` W )
ipass.p 
|- .X. = ( .r ` F )
ipassr.i 
|- .* = ( *r ` F )
Assertion ipassr 
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( A ., ( C .x. B ) ) = ( ( A ., B ) .X. ( .* ` C ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f 
 |-  F = ( Scalar ` W )
2 phllmhm.h 
 |-  ., = ( .i ` W )
3 phllmhm.v 
 |-  V = ( Base ` W )
4 ipdir.f 
 |-  K = ( Base ` F )
5 ipass.s 
 |-  .x. = ( .s ` W )
6 ipass.p 
 |-  .X. = ( .r ` F )
7 ipassr.i 
 |-  .* = ( *r ` F )
8 simpl 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> W e. PreHil )
9 simpr3 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> C e. K )
10 simpr2 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> B e. V )
11 simpr1 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> A e. V )
12 1 2 3 4 5 6 ipass 
 |-  ( ( W e. PreHil /\ ( C e. K /\ B e. V /\ A e. V ) ) -> ( ( C .x. B ) ., A ) = ( C .X. ( B ., A ) ) )
13 8 9 10 11 12 syl13anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( ( C .x. B ) ., A ) = ( C .X. ( B ., A ) ) )
14 13 fveq2d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( .* ` ( ( C .x. B ) ., A ) ) = ( .* ` ( C .X. ( B ., A ) ) ) )
15 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
16 15 adantr 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> W e. LMod )
17 3 1 5 4 lmodvscl 
 |-  ( ( W e. LMod /\ C e. K /\ B e. V ) -> ( C .x. B ) e. V )
18 16 9 10 17 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( C .x. B ) e. V )
19 1 2 3 7 ipcj 
 |-  ( ( W e. PreHil /\ ( C .x. B ) e. V /\ A e. V ) -> ( .* ` ( ( C .x. B ) ., A ) ) = ( A ., ( C .x. B ) ) )
20 8 18 11 19 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( .* ` ( ( C .x. B ) ., A ) ) = ( A ., ( C .x. B ) ) )
21 1 phlsrng 
 |-  ( W e. PreHil -> F e. *Ring )
22 21 adantr 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> F e. *Ring )
23 1 2 3 4 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( B ., A ) e. K )
24 8 10 11 23 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( B ., A ) e. K )
25 7 4 6 srngmul 
 |-  ( ( F e. *Ring /\ C e. K /\ ( B ., A ) e. K ) -> ( .* ` ( C .X. ( B ., A ) ) ) = ( ( .* ` ( B ., A ) ) .X. ( .* ` C ) ) )
26 22 9 24 25 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( .* ` ( C .X. ( B ., A ) ) ) = ( ( .* ` ( B ., A ) ) .X. ( .* ` C ) ) )
27 14 20 26 3eqtr3d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( A ., ( C .x. B ) ) = ( ( .* ` ( B ., A ) ) .X. ( .* ` C ) ) )
28 1 2 3 7 ipcj 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( .* ` ( B ., A ) ) = ( A ., B ) )
29 8 10 11 28 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( .* ` ( B ., A ) ) = ( A ., B ) )
30 29 oveq1d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( ( .* ` ( B ., A ) ) .X. ( .* ` C ) ) = ( ( A ., B ) .X. ( .* ` C ) ) )
31 27 30 eqtrd 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. K ) ) -> ( A ., ( C .x. B ) ) = ( ( A ., B ) .X. ( .* ` C ) ) )