MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringdir Structured version   Visualization version   GIF version

Theorem ringdir 20279
Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
Hypotheses
Ref Expression
ringdi.b 𝐵 = (Base‘𝑅)
ringdi.p + = (+g𝑅)
ringdi.t · = (.r𝑅)
Assertion
Ref Expression
ringdir ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))

Proof of Theorem ringdir
StepHypRef Expression
1 ringdi.b . . 3 𝐵 = (Base‘𝑅)
2 ringdi.p . . 3 + = (+g𝑅)
3 ringdi.t . . 3 · = (.r𝑅)
41, 2, 3ringdilem 20267 . 2 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))
54simprd 495 1 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1537  wcel 2106  cfv 6563  (class class class)co 7431  Basecbs 17245  +gcplusg 17298  .rcmulr 17299  Ringcrg 20251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706  ax-nul 5312
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-ring 20253
This theorem is referenced by:  ringo2times  20289  ringcomlem  20293  ringnegl  20316  mulgass2  20323  ringrghm  20327  prdsringd  20335  imasring  20344  dvrdir  20429  issubrg2  20609  cntzsubr  20623  sralmod  21212  frlmphl  21819  psrlmod  21998  psrdir  22004  evlslem1  22124  mamudi  22423  mdetrlin  22624  ringdird  33220  rlocaddval  33255  mxidlprm  33478  q1pdir  33603  r1pcyc  33607  lflvscl  39059  lflvsdi1  39060  dvhlveclem  41091
  Copyright terms: Public domain W3C validator