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

Theorem ring0cl 19318
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 19298 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ring0cl.b . . 3 𝐵 = (Base‘𝑅)
3 ring0cl.z . . 3 0 = (0g𝑅)
42, 3grpidcl 18126 . 2 (𝑅 ∈ Grp → 0𝐵)
51, 4syl 17 1 (𝑅 ∈ Ring → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  cfv 6328  Basecbs 16478  0gc0g 16708  Grpcgrp 18098  Ringcrg 19293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-riota 7097  df-ov 7142  df-0g 16710  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-grp 18101  df-ring 19295
This theorem is referenced by:  dvdsr01  19404  dvdsr02  19405  irredn0  19452  cntzsubr  19564  abv0  19598  abvtrivd  19607  lmod0cl  19656  lmod0vs  19663  lmodvs0  19664  lpi0  20016  isnzr2  20032  isnzr2hash  20033  ringelnzr  20035  0ring  20039  01eq0ring  20041  ringen1zr  20046  frlmphllem  20472  frlmphl  20473  uvcvvcl2  20480  uvcff  20483  psr1cl  20643  mvrf  20665  mplmon  20706  mplmonmul  20707  mplcoe1  20708  evlslem3  20755  coe1z  20895  coe1tmfv2  20907  ply1scl0  20922  ply1scln0  20923  gsummoncoe1  20936  mamumat1cl  21047  dmatsubcl  21106  dmatmulcl  21108  scmatscmiddistr  21116  marrepcl  21172  mdetr0  21213  mdetunilem8  21227  mdetunilem9  21228  maducoeval2  21248  maduf  21249  madutpos  21250  madugsum  21251  marep01ma  21268  smadiadetlem4  21277  smadiadetglem2  21280  1elcpmat  21323  m2cpminv0  21369  decpmataa0  21376  monmatcollpw  21387  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  chfacfisf  21462  cphsubrglem  23785  mdegaddle  24678  ply1divex  24740  facth1  24768  fta1blem  24772  abvcxp  26202  rhmpreimaidl  31014  elrspunidl  31017  qsidomlem2  31037  lfl0sc  36371  lflsc0N  36372  baerlem3lem1  38996  selvval2lem4  39418  frlmpwfi  40029  mnringmulrcld  40923  zrrnghm  44528  zlidlring  44539  cznrng  44566  linc0scn0  44819  linc1  44821
  Copyright terms: Public domain W3C validator