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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C + D = A ⁢ C + D ⁢ B + A ⁢ D + C ⁢ B

Proof

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