Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  srgrz Structured version   Unicode version

Theorem srgrz 16744
 Description: The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.)
Hypotheses
Ref Expression
srgz.b
srgz.t
srgz.z
Assertion
Ref Expression
srgrz SRing

Proof of Theorem srgrz
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srgz.b . . . . . . . 8
2 eqid 2452 . . . . . . . 8 mulGrp mulGrp
3 eqid 2452 . . . . . . . 8
4 srgz.t . . . . . . . 8
5 srgz.z . . . . . . . 8
61, 2, 3, 4, 5issrg 16726 . . . . . . 7 SRing CMnd mulGrp
76simp3bi 1005 . . . . . 6 SRing
87r19.21bi 2914 . . . . 5 SRing
98simprd 463 . . . 4 SRing
109simprd 463 . . 3 SRing
1110ralrimiva 2827 . 2 SRing
12 oveq1 6202 . . . 4
1312eqeq1d 2454 . . 3
1413rspcv 3169 . 2
1511, 14mpan9 469 1 SRing
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1370   wcel 1758  wral 2796  cfv 5521  (class class class)co 6195  cbs 14287   cplusg 14352  cmulr 14353  c0g 14492  cmnd 15523  CMndccmn 16393  mulGrpcmgp 16708  SRingcsrg 16724 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-nul 4524 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-sbc 3289  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-br 4396  df-iota 5484  df-fv 5529  df-ov 6198  df-srg 16725 This theorem is referenced by:  srgisid  16746  srglmhm  16751  slmdvs0  26381
 Copyright terms: Public domain W3C validator