Metamath Proof Explorer

Theorem muladd

Description: Product of two sums. (Contributed by NM, 14-Jan-2006) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2 adddi ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 + 𝐵 ) · 𝐶 ) + ( ( 𝐴 + 𝐵 ) · 𝐷 ) ) )
3 2 3expb ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 + 𝐵 ) · 𝐶 ) + ( ( 𝐴 + 𝐵 ) · 𝐷 ) ) )
4 1 3 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 + 𝐵 ) · 𝐶 ) + ( ( 𝐴 + 𝐵 ) · 𝐷 ) ) )
5 adddir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) )
6 5 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) )
7 6 adantrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) )
8 adddir ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) )
9 8 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) )
10 9 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) )
11 7 10 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) · 𝐶 ) + ( ( 𝐴 + 𝐵 ) · 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
12 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
13 12 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
14 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
15 14 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
16 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
17 mulcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
18 addcl ⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐵 · 𝐷 ) ∈ ℂ ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
19 16 17 18 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
20 19 anandirs ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
21 20 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
22 13 15 21 add32d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( ( 𝐴 · 𝐶 ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐵 · 𝐶 ) ) )
23 mulcom ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐵 · 𝐷 ) = ( 𝐷 · 𝐵 ) )
24 23 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐷 ) = ( 𝐷 · 𝐵 ) )
25 24 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) + ( 𝐵 · 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) + ( 𝐷 · 𝐵 ) ) )
26 16 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
27 17 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
28 13 26 27 addassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) + ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
29 mulcl ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐷 · 𝐵 ) ∈ ℂ )
30 29 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐷 · 𝐵 ) ∈ ℂ )
31 30 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐷 · 𝐵 ) ∈ ℂ )
32 13 26 31 add32d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) + ( 𝐷 · 𝐵 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( 𝐴 · 𝐷 ) ) )
33 25 28 32 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( 𝐴 · 𝐷 ) ) )
34 mulcom ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
35 34 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
36 33 35 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) + ( 𝐵 · 𝐶 ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( 𝐴 · 𝐷 ) ) + ( 𝐶 · 𝐵 ) ) )
37 addcl ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐷 · 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
38 12 30 37 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
39 38 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) ∈ ℂ )
40 mulcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
41 40 ancoms ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
42 41 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
43 39 26 42 addassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( 𝐴 · 𝐷 ) ) + ( 𝐶 · 𝐵 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )
44 22 36 43 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )
45 4 11 44 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐷 · 𝐵 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) )