Metamath Proof Explorer

Theorem ipass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (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 )
Assertion ipass 
|- ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A .X. ( B ., 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 eqid 
 |-  ( x e. V |-> ( x ., C ) ) = ( x e. V |-> ( x ., C ) )
8 1 2 3 7 phllmhm 
 |-  ( ( W e. PreHil /\ C e. V ) -> ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) )
9 8 3ad2antr3 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) )
10 simpr1 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> A e. K )
11 simpr2 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> B e. V )
12 rlmvsca 
 |-  ( .r ` F ) = ( .s ` ( ringLMod ` F ) )
13 6 12 eqtri 
 |-  .X. = ( .s ` ( ringLMod ` F ) )
14 1 4 3 5 13 lmhmlin 
 |-  ( ( ( x e. V |-> ( x ., C ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ A e. K /\ B e. V ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .x. B ) ) = ( A .X. ( ( x e. V |-> ( x ., C ) ) ` B ) ) )
15 9 10 11 14 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .x. B ) ) = ( A .X. ( ( x e. V |-> ( x ., C ) ) ` B ) ) )
16 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
17 16 adantr 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> W e. LMod )
18 3 1 5 4 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ B e. V ) -> ( A .x. B ) e. V )
19 17 10 11 18 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( A .x. B ) e. V )
20 oveq1 
 |-  ( x = ( A .x. B ) -> ( x ., C ) = ( ( A .x. B ) ., C ) )
21 ovex 
 |-  ( x ., C ) e. _V
22 20 7 21 fvmpt3i 
 |-  ( ( A .x. B ) e. V -> ( ( x e. V |-> ( x ., C ) ) ` ( A .x. B ) ) = ( ( A .x. B ) ., C ) )
23 19 22 syl 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` ( A .x. B ) ) = ( ( A .x. B ) ., C ) )
24 oveq1 
 |-  ( x = B -> ( x ., C ) = ( B ., C ) )
25 24 7 21 fvmpt3i 
 |-  ( B e. V -> ( ( x e. V |-> ( x ., C ) ) ` B ) = ( B ., C ) )
26 11 25 syl 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( x e. V |-> ( x ., C ) ) ` B ) = ( B ., C ) )
27 26 oveq2d 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( A .X. ( ( x e. V |-> ( x ., C ) ) ` B ) ) = ( A .X. ( B ., C ) ) )
28 15 23 27 3eqtr3d 
 |-  ( ( W e. PreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A .X. ( B ., C ) ) )