Metamath Proof Explorer

Theorem cph2subdi

Description: Distributive law for inner product subtraction. Complex version of ip2subdi . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h 
|- ., = ( .i ` W )
cphipcj.v 
|- V = ( Base ` W )
cphsubdir.m 
|- .- = ( -g ` W )
cph2subdi.1 
|- ( ph -> W e. CPreHil )
cph2subdi.2 
|- ( ph -> A e. V )
cph2subdi.3 
|- ( ph -> B e. V )
cph2subdi.4 
|- ( ph -> C e. V )
cph2subdi.5 
|- ( ph -> D e. V )
Assertion cph2subdi 
|- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h 
 |-  ., = ( .i ` W )
2 cphipcj.v 
 |-  V = ( Base ` W )
3 cphsubdir.m 
 |-  .- = ( -g ` W )
4 cph2subdi.1 
 |-  ( ph -> W e. CPreHil )
5 cph2subdi.2 
 |-  ( ph -> A e. V )
6 cph2subdi.3 
 |-  ( ph -> B e. V )
7 cph2subdi.4 
 |-  ( ph -> C e. V )
8 cph2subdi.5 
 |-  ( ph -> D e. V )
9 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
10 4 9 syl 
 |-  ( ph -> W e. CMod )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 11 clmadd 
 |-  ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
13 10 12 syl 
 |-  ( ph -> + = ( +g ` ( Scalar ` W ) ) )
14 13 oveqd 
 |-  ( ph -> ( ( A ., C ) + ( B ., D ) ) = ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) )
15 13 oveqd 
 |-  ( ph -> ( ( A ., D ) + ( B ., C ) ) = ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) )
16 14 15 oveq12d 
 |-  ( ph -> ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
17 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
18 4 17 syl 
 |-  ( ph -> W e. PreHil )
19 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
20 11 1 2 19 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
21 18 5 7 20 syl3anc 
 |-  ( ph -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
22 11 1 2 19 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ D e. V ) -> ( B ., D ) e. ( Base ` ( Scalar ` W ) ) )
23 18 6 8 22 syl3anc 
 |-  ( ph -> ( B ., D ) e. ( Base ` ( Scalar ` W ) ) )
24 11 19 clmacl 
 |-  ( ( W e. CMod /\ ( A ., C ) e. ( Base ` ( Scalar ` W ) ) /\ ( B ., D ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) )
25 10 21 23 24 syl3anc 
 |-  ( ph -> ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) )
26 11 1 2 19 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ D e. V ) -> ( A ., D ) e. ( Base ` ( Scalar ` W ) ) )
27 18 5 8 26 syl3anc 
 |-  ( ph -> ( A ., D ) e. ( Base ` ( Scalar ` W ) ) )
28 11 1 2 19 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
29 18 6 7 28 syl3anc 
 |-  ( ph -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
30 11 19 clmacl 
 |-  ( ( W e. CMod /\ ( A ., D ) e. ( Base ` ( Scalar ` W ) ) /\ ( B ., C ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) )
31 10 27 29 30 syl3anc 
 |-  ( ph -> ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) )
32 11 19 clmsub 
 |-  ( ( W e. CMod /\ ( ( A ., C ) + ( B ., D ) ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( A ., D ) + ( B ., C ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) )
33 10 25 31 32 syl3anc 
 |-  ( ph -> ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) = ( ( ( A ., C ) + ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) + ( B ., C ) ) ) )
34 eqid 
 |-  ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` W ) )
35 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
36 11 1 2 3 34 35 18 5 6 7 8 ip2subdi 
 |-  ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) ( +g ` ( Scalar ` W ) ) ( B ., D ) ) ( -g ` ( Scalar ` W ) ) ( ( A ., D ) ( +g ` ( Scalar ` W ) ) ( B ., C ) ) ) )
37 16 33 36 3eqtr4rd 
 |-  ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) )