Metamath Proof Explorer

Theorem ip2subdi

Description: Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ipsubdir.m 
|- .- = ( -g ` W )
ipsubdir.s 
|- S = ( -g ` F )
ip2subdi.p 
|- .+ = ( +g ` F )
ip2subdi.1 
|- ( ph -> W e. PreHil )
ip2subdi.2 
|- ( ph -> A e. V )
ip2subdi.3 
|- ( ph -> B e. V )
ip2subdi.4 
|- ( ph -> C e. V )
ip2subdi.5 
|- ( ph -> D e. V )
Assertion ip2subdi 
|- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) .+ ( B ., D ) ) S ( ( 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 ipsubdir.m 
 |-  .- = ( -g ` W )
5 ipsubdir.s 
 |-  S = ( -g ` F )
6 ip2subdi.p 
 |-  .+ = ( +g ` F )
7 ip2subdi.1 
 |-  ( ph -> W e. PreHil )
8 ip2subdi.2 
 |-  ( ph -> A e. V )
9 ip2subdi.3 
 |-  ( ph -> B e. V )
10 ip2subdi.4 
 |-  ( ph -> C e. V )
11 ip2subdi.5 
 |-  ( ph -> D e. V )
12 eqid 
 |-  ( Base ` F ) = ( Base ` F )
13 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
14 7 13 syl 
 |-  ( ph -> W e. LMod )
15 1 lmodring 
 |-  ( W e. LMod -> F e. Ring )
16 14 15 syl 
 |-  ( ph -> F e. Ring )
17 ringabl 
 |-  ( F e. Ring -> F e. Abel )
18 16 17 syl 
 |-  ( ph -> F e. Abel )
19 1 2 3 12 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` F ) )
20 7 8 10 19 syl3anc 
 |-  ( ph -> ( A ., C ) e. ( Base ` F ) )
21 1 2 3 12 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ D e. V ) -> ( A ., D ) e. ( Base ` F ) )
22 7 8 11 21 syl3anc 
 |-  ( ph -> ( A ., D ) e. ( Base ` F ) )
23 1 2 3 12 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. ( Base ` F ) )
24 7 9 10 23 syl3anc 
 |-  ( ph -> ( B ., C ) e. ( Base ` F ) )
25 12 6 5 18 20 22 24 ablsubsub4 
 |-  ( ph -> ( ( ( A ., C ) S ( A ., D ) ) S ( B ., C ) ) = ( ( A ., C ) S ( ( A ., D ) .+ ( B ., C ) ) ) )
26 25 oveq1d 
 |-  ( ph -> ( ( ( ( A ., C ) S ( A ., D ) ) S ( B ., C ) ) .+ ( B ., D ) ) = ( ( ( A ., C ) S ( ( A ., D ) .+ ( B ., C ) ) ) .+ ( B ., D ) ) )
27 3 4 lmodvsubcl 
 |-  ( ( W e. LMod /\ C e. V /\ D e. V ) -> ( C .- D ) e. V )
28 14 10 11 27 syl3anc 
 |-  ( ph -> ( C .- D ) e. V )
29 1 2 3 4 5 ipsubdir 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ ( C .- D ) e. V ) ) -> ( ( A .- B ) ., ( C .- D ) ) = ( ( A ., ( C .- D ) ) S ( B ., ( C .- D ) ) ) )
30 7 8 9 28 29 syl13anc 
 |-  ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( A ., ( C .- D ) ) S ( B ., ( C .- D ) ) ) )
31 1 2 3 4 5 ipsubdi 
 |-  ( ( W e. PreHil /\ ( A e. V /\ C e. V /\ D e. V ) ) -> ( A ., ( C .- D ) ) = ( ( A ., C ) S ( A ., D ) ) )
32 7 8 10 11 31 syl13anc 
 |-  ( ph -> ( A ., ( C .- D ) ) = ( ( A ., C ) S ( A ., D ) ) )
33 1 2 3 4 5 ipsubdi 
 |-  ( ( W e. PreHil /\ ( B e. V /\ C e. V /\ D e. V ) ) -> ( B ., ( C .- D ) ) = ( ( B ., C ) S ( B ., D ) ) )
34 7 9 10 11 33 syl13anc 
 |-  ( ph -> ( B ., ( C .- D ) ) = ( ( B ., C ) S ( B ., D ) ) )
35 32 34 oveq12d 
 |-  ( ph -> ( ( A ., ( C .- D ) ) S ( B ., ( C .- D ) ) ) = ( ( ( A ., C ) S ( A ., D ) ) S ( ( B ., C ) S ( B ., D ) ) ) )
36 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
37 16 36 syl 
 |-  ( ph -> F e. Grp )
38 12 5 grpsubcl 
 |-  ( ( F e. Grp /\ ( A ., C ) e. ( Base ` F ) /\ ( A ., D ) e. ( Base ` F ) ) -> ( ( A ., C ) S ( A ., D ) ) e. ( Base ` F ) )
39 37 20 22 38 syl3anc 
 |-  ( ph -> ( ( A ., C ) S ( A ., D ) ) e. ( Base ` F ) )
40 1 2 3 12 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ D e. V ) -> ( B ., D ) e. ( Base ` F ) )
41 7 9 11 40 syl3anc 
 |-  ( ph -> ( B ., D ) e. ( Base ` F ) )
42 12 6 5 18 39 24 41 ablsubsub 
 |-  ( ph -> ( ( ( A ., C ) S ( A ., D ) ) S ( ( B ., C ) S ( B ., D ) ) ) = ( ( ( ( A ., C ) S ( A ., D ) ) S ( B ., C ) ) .+ ( B ., D ) ) )
43 30 35 42 3eqtrd 
 |-  ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( ( A ., C ) S ( A ., D ) ) S ( B ., C ) ) .+ ( B ., D ) ) )
44 12 6 ringacl 
 |-  ( ( F e. Ring /\ ( A ., D ) e. ( Base ` F ) /\ ( B ., C ) e. ( Base ` F ) ) -> ( ( A ., D ) .+ ( B ., C ) ) e. ( Base ` F ) )
45 16 22 24 44 syl3anc 
 |-  ( ph -> ( ( A ., D ) .+ ( B ., C ) ) e. ( Base ` F ) )
46 12 6 5 abladdsub 
 |-  ( ( F e. Abel /\ ( ( A ., C ) e. ( Base ` F ) /\ ( B ., D ) e. ( Base ` F ) /\ ( ( A ., D ) .+ ( B ., C ) ) e. ( Base ` F ) ) ) -> ( ( ( A ., C ) .+ ( B ., D ) ) S ( ( A ., D ) .+ ( B ., C ) ) ) = ( ( ( A ., C ) S ( ( A ., D ) .+ ( B ., C ) ) ) .+ ( B ., D ) ) )
47 18 20 41 45 46 syl13anc 
 |-  ( ph -> ( ( ( A ., C ) .+ ( B ., D ) ) S ( ( A ., D ) .+ ( B ., C ) ) ) = ( ( ( A ., C ) S ( ( A ., D ) .+ ( B ., C ) ) ) .+ ( B ., D ) ) )
48 26 43 47 3eqtr4d 
 |-  ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) .+ ( B ., D ) ) S ( ( A ., D ) .+ ( B ., C ) ) ) )