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

Theorem srglz 16735
 Description: The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.)
Hypotheses
Ref Expression
srgz.b
srgz.t
srgz.z
Assertion
Ref Expression
srglz SRing

Proof of Theorem srglz
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srgz.b . . . . . . . 8
2 eqid 2451 . . . . . . . 8 mulGrp mulGrp
3 eqid 2451 . . . . . . . 8
4 srgz.t . . . . . . . 8
5 srgz.z . . . . . . . 8
61, 2, 3, 4, 5issrg 16716 . . . . . . 7 SRing CMnd mulGrp
76simp3bi 1005 . . . . . 6 SRing
87r19.21bi 2912 . . . . 5 SRing
98simprd 463 . . . 4 SRing
109simpld 459 . . 3 SRing
1110ralrimiva 2822 . 2 SRing
12 oveq2 6200 . . . 4
1312eqeq1d 2453 . . 3
1413rspcv 3167 . 2
1511, 14mpan9 469 1 SRing
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1370   wcel 1758  wral 2795  cfv 5518  (class class class)co 6192  cbs 14278   cplusg 14342  cmulr 14343  c0g 14482  cmnd 15513  CMndccmn 16383  mulGrpcmgp 16698  SRingcsrg 16714 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 1952  ax-ext 2430  ax-nul 4521 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 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-sbc 3287  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-iota 5481  df-fv 5526  df-ov 6195  df-srg 16715 This theorem is referenced by:  srgmulgass  16737  srgrmhm  16742
 Copyright terms: Public domain W3C validator