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

Theorem ringdir 18507
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, 3ringi 18500 . 2 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))
54simprd 479 1 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  cfv 5857  (class class class)co 6615  Basecbs 15800  +gcplusg 15881  .rcmulr 15882  Ringcrg 18487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-ring 18489
This theorem is referenced by:  ringadd2  18515  rngo2times  18516  ringcom  18519  ringlz  18527  ringnegl  18534  rngsubdir  18540  mulgass2  18541  ringrghm  18545  prdsringd  18552  imasring  18559  opprring  18571  issubrg2  18740  cntzsubr  18752  sralmod  19127  psrlmod  19341  psrdir  19347  evlslem1  19455  frlmphl  20060  mamudi  20149  mdetrlin  20348  dvrdir  29617  lflvscl  33883  lflvsdi1  33884  dvhlveclem  35916  lidlrng  41245
  Copyright terms: Public domain W3C validator