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

Theorem ringdir 19442
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 19435 . 2 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))))
54simprd 499 1 ((𝑅 ∈ Ring ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088   = wceq 1542  wcel 2114  cfv 6340  (class class class)co 7173  Basecbs 16589  +gcplusg 16671  .rcmulr 16672  Ringcrg 19419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-nul 5175
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3401  df-sbc 3682  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7176  df-ring 19421
This theorem is referenced by:  ringadd2  19450  rngo2times  19451  ringcom  19454  ringlz  19462  ringnegl  19469  rngsubdir  19475  mulgass2  19476  ringrghm  19480  prdsringd  19487  imasring  19494  opprring  19506  issubrg2  19677  cntzsubr  19690  sralmod  20081  frlmphl  20600  psrlmod  20783  psrdir  20789  evlslem1  20899  mamudi  21157  mdetrlin  21356  dvrdir  31067  mxidlprm  31215  lflvscl  36737  lflvsdi1  36738  dvhlveclem  38768  lidlrng  45049
  Copyright terms: Public domain W3C validator