Metamath Proof Explorer

Theorem mulsub

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

Ref Expression
Assertion mulsub ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 negsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
2 negsub ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 + - 𝐷 ) = ( 𝐶 − 𝐷 ) )
3 1 2 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + - 𝐵 ) · ( 𝐶 + - 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) )
4 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
5 negcl ⊢ ( 𝐷 ∈ ℂ → - 𝐷 ∈ ℂ )
6 muladd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ - 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + - 𝐵 ) · ( 𝐶 + - 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) + ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) ) )
7 5 6 sylanr2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + - 𝐵 ) · ( 𝐶 + - 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) + ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) ) )
8 4 7 sylanl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + - 𝐵 ) · ( 𝐶 + - 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) + ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) ) )
9 mul2neg ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐷 · - 𝐵 ) = ( 𝐷 · 𝐵 ) )
10 9 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( - 𝐷 · - 𝐵 ) = ( 𝐷 · 𝐵 ) )
11 10 oveq2d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) )
12 11 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) )
13 mulneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 · - 𝐷 ) = - ( 𝐴 · 𝐷 ) )
14 mulneg2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 · - 𝐵 ) = - ( 𝐶 · 𝐵 ) )
15 13 14 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) = ( - ( 𝐴 · 𝐷 ) + - ( 𝐶 · 𝐵 ) ) )
16 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
17 mulcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
18 negdi ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) = ( - ( 𝐴 · 𝐷 ) + - ( 𝐶 · 𝐵 ) ) )
19 16 17 18 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) = ( - ( 𝐴 · 𝐷 ) + - ( 𝐶 · 𝐵 ) ) )
20 15 19 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) = - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
21 20 ancom2s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) = - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
22 21 an42s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) = - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) )
23 12 22 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( - 𝐷 · - 𝐵 ) ) + ( ( 𝐴 · - 𝐷 ) + ( 𝐶 · - 𝐵 ) ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )
24 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
25 mulcl ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐷 · 𝐵 ) ∈ ℂ )
26 25 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐷 · 𝐵 ) ∈ ℂ )
27 addcl ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐷 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
28 24 26 27 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
29 28 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
30 17 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
31 addcl ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ )
32 16 30 31 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ )
33 32 an42s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ )
34 29 33 negsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + - ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )
35 8 23 34 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + - 𝐵 ) · ( 𝐶 + - 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )
36 3 35 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )