This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulsub

Description: Product of two differences. (Contributed by NM, 14-Jan-2006)

Ref Expression
Assertion mulsub 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )

Proof

Step Hyp Ref Expression
1 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
2 negsub 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C + -u D ) = ( C - D ) )
3 1 2 oveqan12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + -u B ) x. ( C + -u D ) ) = ( ( A - B ) x. ( C - D ) ) )
4 negcl 
 |-  ( B e. CC -> -u B e. CC )
5 negcl 
 |-  ( D e. CC -> -u D e. CC )
6 muladd 
 |-  ( ( ( A e. CC /\ -u B e. CC ) /\ ( C e. CC /\ -u D e. CC ) ) -> ( ( A + -u B ) x. ( C + -u D ) ) = ( ( ( A x. C ) + ( -u D x. -u B ) ) + ( ( A x. -u D ) + ( C x. -u B ) ) ) )
7 5 6 sylanr2 
 |-  ( ( ( A e. CC /\ -u B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + -u B ) x. ( C + -u D ) ) = ( ( ( A x. C ) + ( -u D x. -u B ) ) + ( ( A x. -u D ) + ( C x. -u B ) ) ) )
8 4 7 sylanl2 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + -u B ) x. ( C + -u D ) ) = ( ( ( A x. C ) + ( -u D x. -u B ) ) + ( ( A x. -u D ) + ( C x. -u B ) ) ) )
9 mul2neg 
 |-  ( ( D e. CC /\ B e. CC ) -> ( -u D x. -u B ) = ( D x. B ) )
10 9 ancoms 
 |-  ( ( B e. CC /\ D e. CC ) -> ( -u D x. -u B ) = ( D x. B ) )
11 10 oveq2d 
 |-  ( ( B e. CC /\ D e. CC ) -> ( ( A x. C ) + ( -u D x. -u B ) ) = ( ( A x. C ) + ( D x. B ) ) )
12 11 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( -u D x. -u B ) ) = ( ( A x. C ) + ( D x. B ) ) )
13 mulneg2 
 |-  ( ( A e. CC /\ D e. CC ) -> ( A x. -u D ) = -u ( A x. D ) )
14 mulneg2 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C x. -u B ) = -u ( C x. B ) )
15 13 14 oveqan12d 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( C e. CC /\ B e. CC ) ) -> ( ( A x. -u D ) + ( C x. -u B ) ) = ( -u ( A x. D ) + -u ( C x. B ) ) )
16 mulcl 
 |-  ( ( A e. CC /\ D e. CC ) -> ( A x. D ) e. CC )
17 mulcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C x. B ) e. CC )
18 negdi 
 |-  ( ( ( A x. D ) e. CC /\ ( C x. B ) e. CC ) -> -u ( ( A x. D ) + ( C x. B ) ) = ( -u ( A x. D ) + -u ( C x. B ) ) )
19 16 17 18 syl2an 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( C e. CC /\ B e. CC ) ) -> -u ( ( A x. D ) + ( C x. B ) ) = ( -u ( A x. D ) + -u ( C x. B ) ) )
20 15 19 eqtr4d 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( C e. CC /\ B e. CC ) ) -> ( ( A x. -u D ) + ( C x. -u B ) ) = -u ( ( A x. D ) + ( C x. B ) ) )
21 20 ancom2s 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( B e. CC /\ C e. CC ) ) -> ( ( A x. -u D ) + ( C x. -u B ) ) = -u ( ( A x. D ) + ( C x. B ) ) )
22 21 an42s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. -u D ) + ( C x. -u B ) ) = -u ( ( A x. D ) + ( C x. B ) ) )
23 12 22 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( -u D x. -u B ) ) + ( ( A x. -u D ) + ( C x. -u B ) ) ) = ( ( ( A x. C ) + ( D x. B ) ) + -u ( ( A x. D ) + ( C x. B ) ) ) )
24 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
25 mulcl 
 |-  ( ( D e. CC /\ B e. CC ) -> ( D x. B ) e. CC )
26 25 ancoms 
 |-  ( ( B e. CC /\ D e. CC ) -> ( D x. B ) e. CC )
27 addcl 
 |-  ( ( ( A x. C ) e. CC /\ ( D x. B ) e. CC ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
28 24 26 27 syl2an 
 |-  ( ( ( A e. CC /\ C e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
29 28 an4s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. C ) + ( D x. B ) ) e. CC )
30 17 ancoms 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C x. B ) e. CC )
31 addcl 
 |-  ( ( ( A x. D ) e. CC /\ ( C x. B ) e. CC ) -> ( ( A x. D ) + ( C x. B ) ) e. CC )
32 16 30 31 syl2an 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( B e. CC /\ C e. CC ) ) -> ( ( A x. D ) + ( C x. B ) ) e. CC )
33 32 an42s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. D ) + ( C x. B ) ) e. CC )
34 29 33 negsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A x. C ) + ( D x. B ) ) + -u ( ( A x. D ) + ( C x. B ) ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
35 8 23 34 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + -u B ) x. ( C + -u D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
36 3 35 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )