Metamath Proof Explorer

Theorem ip2di

Description: Distributive law for inner product. (Contributed by NM, 17-Apr-2008) (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 )
ip2di.1 
|- ( ph -> W e. PreHil )
ip2di.2 
|- ( ph -> A e. V )
ip2di.3 
|- ( ph -> B e. V )
ip2di.4 
|- ( ph -> C e. V )
ip2di.5 
|- ( ph -> D e. V )
Assertion ip2di 
|- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) .+^ ( B ., D ) ) .+^ ( ( A ., D ) .+^ ( 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.g 
 |-  .+ = ( +g ` W )
5 ipdir.p 
 |-  .+^ = ( +g ` F )
6 ip2di.1 
 |-  ( ph -> W e. PreHil )
7 ip2di.2 
 |-  ( ph -> A e. V )
8 ip2di.3 
 |-  ( ph -> B e. V )
9 ip2di.4 
 |-  ( ph -> C e. V )
10 ip2di.5 
 |-  ( ph -> D e. V )
11 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
12 6 11 syl 
 |-  ( ph -> W e. LMod )
13 3 4 lmodvacl 
 |-  ( ( W e. LMod /\ C e. V /\ D e. V ) -> ( C .+ D ) e. V )
14 12 9 10 13 syl3anc 
 |-  ( ph -> ( C .+ D ) e. V )
15 1 2 3 4 5 ipdir 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ ( C .+ D ) e. V ) ) -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( A ., ( C .+ D ) ) .+^ ( B ., ( C .+ D ) ) ) )
16 6 7 8 14 15 syl13anc 
 |-  ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( A ., ( C .+ D ) ) .+^ ( B ., ( C .+ D ) ) ) )
17 1 2 3 4 5 ipdi 
 |-  ( ( W e. PreHil /\ ( A e. V /\ C e. V /\ D e. V ) ) -> ( A ., ( C .+ D ) ) = ( ( A ., C ) .+^ ( A ., D ) ) )
18 6 7 9 10 17 syl13anc 
 |-  ( ph -> ( A ., ( C .+ D ) ) = ( ( A ., C ) .+^ ( A ., D ) ) )
19 1 2 3 4 5 ipdi 
 |-  ( ( W e. PreHil /\ ( B e. V /\ C e. V /\ D e. V ) ) -> ( B ., ( C .+ D ) ) = ( ( B ., C ) .+^ ( B ., D ) ) )
20 6 8 9 10 19 syl13anc 
 |-  ( ph -> ( B ., ( C .+ D ) ) = ( ( B ., C ) .+^ ( B ., D ) ) )
21 1 phlsrng 
 |-  ( W e. PreHil -> F e. *Ring )
22 srngring 
 |-  ( F e. *Ring -> F e. Ring )
23 ringcmn 
 |-  ( F e. Ring -> F e. CMnd )
24 6 21 22 23 4syl 
 |-  ( ph -> F e. CMnd )
25 eqid 
 |-  ( Base ` F ) = ( Base ` F )
26 1 2 3 25 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. ( Base ` F ) )
27 6 8 9 26 syl3anc 
 |-  ( ph -> ( B ., C ) e. ( Base ` F ) )
28 1 2 3 25 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ D e. V ) -> ( B ., D ) e. ( Base ` F ) )
29 6 8 10 28 syl3anc 
 |-  ( ph -> ( B ., D ) e. ( Base ` F ) )
30 25 5 cmncom 
 |-  ( ( F e. CMnd /\ ( B ., C ) e. ( Base ` F ) /\ ( B ., D ) e. ( Base ` F ) ) -> ( ( B ., C ) .+^ ( B ., D ) ) = ( ( B ., D ) .+^ ( B ., C ) ) )
31 24 27 29 30 syl3anc 
 |-  ( ph -> ( ( B ., C ) .+^ ( B ., D ) ) = ( ( B ., D ) .+^ ( B ., C ) ) )
32 20 31 eqtrd 
 |-  ( ph -> ( B ., ( C .+ D ) ) = ( ( B ., D ) .+^ ( B ., C ) ) )
33 18 32 oveq12d 
 |-  ( ph -> ( ( A ., ( C .+ D ) ) .+^ ( B ., ( C .+ D ) ) ) = ( ( ( A ., C ) .+^ ( A ., D ) ) .+^ ( ( B ., D ) .+^ ( B ., C ) ) ) )
34 1 2 3 25 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` F ) )
35 6 7 9 34 syl3anc 
 |-  ( ph -> ( A ., C ) e. ( Base ` F ) )
36 1 2 3 25 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ D e. V ) -> ( A ., D ) e. ( Base ` F ) )
37 6 7 10 36 syl3anc 
 |-  ( ph -> ( A ., D ) e. ( Base ` F ) )
38 25 5 cmn4 
 |-  ( ( F e. CMnd /\ ( ( A ., C ) e. ( Base ` F ) /\ ( A ., D ) e. ( Base ` F ) ) /\ ( ( B ., D ) e. ( Base ` F ) /\ ( B ., C ) e. ( Base ` F ) ) ) -> ( ( ( A ., C ) .+^ ( A ., D ) ) .+^ ( ( B ., D ) .+^ ( B ., C ) ) ) = ( ( ( A ., C ) .+^ ( B ., D ) ) .+^ ( ( A ., D ) .+^ ( B ., C ) ) ) )
39 24 35 37 29 27 38 syl122anc 
 |-  ( ph -> ( ( ( A ., C ) .+^ ( A ., D ) ) .+^ ( ( B ., D ) .+^ ( B ., C ) ) ) = ( ( ( A ., C ) .+^ ( B ., D ) ) .+^ ( ( A ., D ) .+^ ( B ., C ) ) ) )
40 16 33 39 3eqtrd 
 |-  ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) .+^ ( B ., D ) ) .+^ ( ( A ., D ) .+^ ( B ., C ) ) ) )