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

Theorem ring0cl 18550
Description: The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.)
Hypotheses
Ref Expression
ring0cl.b 𝐵 = (Base‘𝑅)
ring0cl.z 0 = (0g𝑅)
Assertion
Ref Expression
ring0cl (𝑅 ∈ Ring → 0𝐵)

Proof of Theorem ring0cl
StepHypRef Expression
1 ringgrp 18533 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ring0cl.b . . 3 𝐵 = (Base‘𝑅)
3 ring0cl.z . . 3 0 = (0g𝑅)
42, 3grpidcl 17431 . 2 (𝑅 ∈ Grp → 0𝐵)
51, 4syl 17 1 (𝑅 ∈ Ring → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  cfv 5876  Basecbs 15838  0gc0g 16081  Grpcgrp 17403  Ringcrg 18528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884  df-riota 6596  df-ov 6638  df-0g 16083  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-grp 17406  df-ring 18530
This theorem is referenced by:  dvdsr01  18636  dvdsr02  18637  irredn0  18684  f1rhm0to0  18721  cntzsubr  18793  abv0  18812  abvtrivd  18821  lmod0cl  18870  lmod0vs  18877  lmodvs0  18878  lpi0  19228  isnzr2  19244  isnzr2hash  19245  ringelnzr  19247  0ring  19251  01eq0ring  19253  ringen1zr  19258  psr1cl  19383  mvrf  19405  mplmon  19444  mplmonmul  19445  mplcoe1  19446  evlslem3  19495  coe1z  19614  coe1tmfv2  19626  ply1scl0  19641  ply1scln0  19642  gsummoncoe1  19655  frlmphllem  20100  frlmphl  20101  uvcvvcl2  20108  uvcff  20111  mamumat1cl  20226  dmatsubcl  20285  dmatmulcl  20287  scmatscmiddistr  20295  marrepcl  20351  mdetr0  20392  mdetunilem8  20406  mdetunilem9  20407  maducoeval2  20427  maduf  20428  madutpos  20429  madugsum  20430  marep01ma  20447  smadiadetlem4  20456  smadiadetglem2  20459  1elcpmat  20501  m2cpminv0  20547  decpmataa0  20554  monmatcollpw  20565  pmatcollpw3fi1lem1  20572  pmatcollpw3fi1lem2  20573  chfacfisf  20640  cphsubrglem  22958  mdegaddle  23815  ply1divex  23877  facth1  23905  fta1blem  23909  abvcxp  25285  lfl0sc  34188  lflsc0N  34189  baerlem3lem1  36815  frlmpwfi  37487  zrrnghm  41682  zlidlring  41693  cznrng  41720  linc0scn0  41977  linc1  41979
  Copyright terms: Public domain W3C validator