ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  muladd Structured version   GIF version

Theorem muladd 7129
Description: Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
muladd (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) · (𝐶 + 𝐷)) = (((A · 𝐶) + (𝐷 · B)) + ((A · 𝐷) + (𝐶 · B))))

Proof of Theorem muladd
StepHypRef Expression
1 addcl 6756 . . 3 ((A B ℂ) → (A + B) ℂ)
2 adddi 6763 . . . 4 (((A + B) 𝐶 𝐷 ℂ) → ((A + B) · (𝐶 + 𝐷)) = (((A + B) · 𝐶) + ((A + B) · 𝐷)))
323expb 1104 . . 3 (((A + B) (𝐶 𝐷 ℂ)) → ((A + B) · (𝐶 + 𝐷)) = (((A + B) · 𝐶) + ((A + B) · 𝐷)))
41, 3sylan 267 . 2 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) · (𝐶 + 𝐷)) = (((A + B) · 𝐶) + ((A + B) · 𝐷)))
5 adddir 6768 . . . . 5 ((A B 𝐶 ℂ) → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶)))
653expa 1103 . . . 4 (((A B ℂ) 𝐶 ℂ) → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶)))
76adantrr 448 . . 3 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶)))
8 adddir 6768 . . . . 5 ((A B 𝐷 ℂ) → ((A + B) · 𝐷) = ((A · 𝐷) + (B · 𝐷)))
983expa 1103 . . . 4 (((A B ℂ) 𝐷 ℂ) → ((A + B) · 𝐷) = ((A · 𝐷) + (B · 𝐷)))
109adantrl 447 . . 3 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) · 𝐷) = ((A · 𝐷) + (B · 𝐷)))
117, 10oveq12d 5470 . 2 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A + B) · 𝐶) + ((A + B) · 𝐷)) = (((A · 𝐶) + (B · 𝐶)) + ((A · 𝐷) + (B · 𝐷))))
12 mulcl 6758 . . . . 5 ((A 𝐶 ℂ) → (A · 𝐶) ℂ)
1312ad2ant2r 478 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → (A · 𝐶) ℂ)
14 mulcl 6758 . . . . 5 ((B 𝐶 ℂ) → (B · 𝐶) ℂ)
1514ad2ant2lr 479 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → (B · 𝐶) ℂ)
16 mulcl 6758 . . . . . . 7 ((A 𝐷 ℂ) → (A · 𝐷) ℂ)
17 mulcl 6758 . . . . . . 7 ((B 𝐷 ℂ) → (B · 𝐷) ℂ)
18 addcl 6756 . . . . . . 7 (((A · 𝐷) (B · 𝐷) ℂ) → ((A · 𝐷) + (B · 𝐷)) ℂ)
1916, 17, 18syl2an 273 . . . . . 6 (((A 𝐷 ℂ) (B 𝐷 ℂ)) → ((A · 𝐷) + (B · 𝐷)) ℂ)
2019anandirs 527 . . . . 5 (((A B ℂ) 𝐷 ℂ) → ((A · 𝐷) + (B · 𝐷)) ℂ)
2120adantrl 447 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A · 𝐷) + (B · 𝐷)) ℂ)
2213, 15, 21add32d 6928 . . 3 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + (B · 𝐶)) + ((A · 𝐷) + (B · 𝐷))) = (((A · 𝐶) + ((A · 𝐷) + (B · 𝐷))) + (B · 𝐶)))
23 mulcom 6760 . . . . . . 7 ((B 𝐷 ℂ) → (B · 𝐷) = (𝐷 · B))
2423ad2ant2l 477 . . . . . 6 (((A B ℂ) (𝐶 𝐷 ℂ)) → (B · 𝐷) = (𝐷 · B))
2524oveq2d 5468 . . . . 5 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + (A · 𝐷)) + (B · 𝐷)) = (((A · 𝐶) + (A · 𝐷)) + (𝐷 · B)))
2616ad2ant2rl 480 . . . . . 6 (((A B ℂ) (𝐶 𝐷 ℂ)) → (A · 𝐷) ℂ)
2717ad2ant2l 477 . . . . . 6 (((A B ℂ) (𝐶 𝐷 ℂ)) → (B · 𝐷) ℂ)
2813, 26, 27addassd 6799 . . . . 5 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + (A · 𝐷)) + (B · 𝐷)) = ((A · 𝐶) + ((A · 𝐷) + (B · 𝐷))))
29 mulcl 6758 . . . . . . . 8 ((𝐷 B ℂ) → (𝐷 · B) ℂ)
3029ancoms 255 . . . . . . 7 ((B 𝐷 ℂ) → (𝐷 · B) ℂ)
3130ad2ant2l 477 . . . . . 6 (((A B ℂ) (𝐶 𝐷 ℂ)) → (𝐷 · B) ℂ)
3213, 26, 31add32d 6928 . . . . 5 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + (A · 𝐷)) + (𝐷 · B)) = (((A · 𝐶) + (𝐷 · B)) + (A · 𝐷)))
3325, 28, 323eqtr3d 2077 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A · 𝐶) + ((A · 𝐷) + (B · 𝐷))) = (((A · 𝐶) + (𝐷 · B)) + (A · 𝐷)))
34 mulcom 6760 . . . . 5 ((B 𝐶 ℂ) → (B · 𝐶) = (𝐶 · B))
3534ad2ant2lr 479 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → (B · 𝐶) = (𝐶 · B))
3633, 35oveq12d 5470 . . 3 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + ((A · 𝐷) + (B · 𝐷))) + (B · 𝐶)) = ((((A · 𝐶) + (𝐷 · B)) + (A · 𝐷)) + (𝐶 · B)))
37 addcl 6756 . . . . . 6 (((A · 𝐶) (𝐷 · B) ℂ) → ((A · 𝐶) + (𝐷 · B)) ℂ)
3812, 30, 37syl2an 273 . . . . 5 (((A 𝐶 ℂ) (B 𝐷 ℂ)) → ((A · 𝐶) + (𝐷 · B)) ℂ)
3938an4s 522 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A · 𝐶) + (𝐷 · B)) ℂ)
40 mulcl 6758 . . . . . 6 ((𝐶 B ℂ) → (𝐶 · B) ℂ)
4140ancoms 255 . . . . 5 ((B 𝐶 ℂ) → (𝐶 · B) ℂ)
4241ad2ant2lr 479 . . . 4 (((A B ℂ) (𝐶 𝐷 ℂ)) → (𝐶 · B) ℂ)
4339, 26, 42addassd 6799 . . 3 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((((A · 𝐶) + (𝐷 · B)) + (A · 𝐷)) + (𝐶 · B)) = (((A · 𝐶) + (𝐷 · B)) + ((A · 𝐷) + (𝐶 · B))))
4422, 36, 433eqtrd 2073 . 2 (((A B ℂ) (𝐶 𝐷 ℂ)) → (((A · 𝐶) + (B · 𝐶)) + ((A · 𝐷) + (B · 𝐷))) = (((A · 𝐶) + (𝐷 · B)) + ((A · 𝐷) + (𝐶 · B))))
454, 11, 443eqtrd 2073 1 (((A B ℂ) (𝐶 𝐷 ℂ)) → ((A + B) · (𝐶 + 𝐷)) = (((A · 𝐶) + (𝐷 · B)) + ((A · 𝐷) + (𝐶 · B))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242   wcel 1390  (class class class)co 5452  cc 6661   + caddc 6666   · cmul 6668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-addcl 6731  ax-mulcl 6733  ax-addcom 6735  ax-mulcom 6736  ax-addass 6737  ax-distr 6739
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-br 3755  df-iota 4809  df-fv 4852  df-ov 5455
This theorem is referenced by:  mulsub  7146  muladdi  7154  muladdd  7161
  Copyright terms: Public domain W3C validator