Metamath Proof Explorer

Theorem ipdi

Description: Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-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.g 
|- .+ = ( +g ` W )
ipdir.p 
|- .+^ = ( +g ` F )
Assertion ipdi 
|- ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) .+^ ( A ., 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.g 
 |-  .+ = ( +g ` W )
5 ipdir.p 
 |-  .+^ = ( +g ` F )
6 simpl 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. PreHil )
7 simpr2 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> B e. V )
8 simpr3 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> C e. V )
9 simpr1 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> A e. V )
10 1 2 3 4 5 ipdir 
 |-  ( ( W e. PreHil /\ ( B e. V /\ C e. V /\ A e. V ) ) -> ( ( B .+ C ) ., A ) = ( ( B ., A ) .+^ ( C ., A ) ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( B .+ C ) ., A ) = ( ( B ., A ) .+^ ( C ., A ) ) )
12 11 fveq2d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( ( B .+ C ) ., A ) ) = ( ( *r ` F ) ` ( ( B ., A ) .+^ ( C ., A ) ) ) )
13 1 phlsrng 
 |-  ( W e. PreHil -> F e. *Ring )
14 13 adantr 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> F e. *Ring )
15 eqid 
 |-  ( Base ` F ) = ( Base ` F )
16 1 2 3 15 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( B ., A ) e. ( Base ` F ) )
17 6 7 9 16 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( B ., A ) e. ( Base ` F ) )
18 1 2 3 15 ipcl 
 |-  ( ( W e. PreHil /\ C e. V /\ A e. V ) -> ( C ., A ) e. ( Base ` F ) )
19 6 8 9 18 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( C ., A ) e. ( Base ` F ) )
20 eqid 
 |-  ( *r ` F ) = ( *r ` F )
21 20 15 5 srngadd 
 |-  ( ( F e. *Ring /\ ( B ., A ) e. ( Base ` F ) /\ ( C ., A ) e. ( Base ` F ) ) -> ( ( *r ` F ) ` ( ( B ., A ) .+^ ( C ., A ) ) ) = ( ( ( *r ` F ) ` ( B ., A ) ) .+^ ( ( *r ` F ) ` ( C ., A ) ) ) )
22 14 17 19 21 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( ( B ., A ) .+^ ( C ., A ) ) ) = ( ( ( *r ` F ) ` ( B ., A ) ) .+^ ( ( *r ` F ) ` ( C ., A ) ) ) )
23 12 22 eqtrd 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( ( B .+ C ) ., A ) ) = ( ( ( *r ` F ) ` ( B ., A ) ) .+^ ( ( *r ` F ) ` ( C ., A ) ) ) )
24 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
25 24 adantr 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. LMod )
26 3 4 lmodvacl 
 |-  ( ( W e. LMod /\ B e. V /\ C e. V ) -> ( B .+ C ) e. V )
27 25 7 8 26 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( B .+ C ) e. V )
28 1 2 3 20 ipcj 
 |-  ( ( W e. PreHil /\ ( B .+ C ) e. V /\ A e. V ) -> ( ( *r ` F ) ` ( ( B .+ C ) ., A ) ) = ( A ., ( B .+ C ) ) )
29 6 27 9 28 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( ( B .+ C ) ., A ) ) = ( A ., ( B .+ C ) ) )
30 1 2 3 20 ipcj 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( ( *r ` F ) ` ( B ., A ) ) = ( A ., B ) )
31 6 7 9 30 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( B ., A ) ) = ( A ., B ) )
32 1 2 3 20 ipcj 
 |-  ( ( W e. PreHil /\ C e. V /\ A e. V ) -> ( ( *r ` F ) ` ( C ., A ) ) = ( A ., C ) )
33 6 8 9 32 syl3anc 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( *r ` F ) ` ( C ., A ) ) = ( A ., C ) )
34 31 33 oveq12d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( *r ` F ) ` ( B ., A ) ) .+^ ( ( *r ` F ) ` ( C ., A ) ) ) = ( ( A ., B ) .+^ ( A ., C ) ) )
35 23 29 34 3eqtr3d 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) .+^ ( A ., C ) ) )