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

Theorem ring0cl 18777
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 18760 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ring0cl.b . . 3 𝐵 = (Base‘𝑅)
3 ring0cl.z . . 3 0 = (0g𝑅)
42, 3grpidcl 17658 . 2 (𝑅 ∈ Grp → 0𝐵)
51, 4syl 17 1 (𝑅 ∈ Ring → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  cfv 6031  Basecbs 16064  0gc0g 16308  Grpcgrp 17630  Ringcrg 18755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-riota 6754  df-ov 6796  df-0g 16310  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-grp 17633  df-ring 18757
This theorem is referenced by:  dvdsr01  18863  dvdsr02  18864  irredn0  18911  f1rhm0to0  18950  cntzsubr  19022  abv0  19041  abvtrivd  19050  lmod0cl  19099  lmod0vs  19106  lmodvs0  19107  lpi0  19462  isnzr2  19478  isnzr2hash  19479  ringelnzr  19481  0ring  19485  01eq0ring  19487  ringen1zr  19492  psr1cl  19617  mvrf  19639  mplmon  19678  mplmonmul  19679  mplcoe1  19680  evlslem3  19729  coe1z  19848  coe1tmfv2  19860  ply1scl0  19875  ply1scln0  19876  gsummoncoe1  19889  frlmphllem  20336  frlmphl  20337  uvcvvcl2  20344  uvcff  20347  mamumat1cl  20462  dmatsubcl  20522  dmatmulcl  20524  scmatscmiddistr  20532  marrepcl  20588  mdetr0  20629  mdetunilem8  20643  mdetunilem9  20644  maducoeval2  20664  maduf  20665  madutpos  20666  madugsum  20667  marep01ma  20685  smadiadetlem4  20694  smadiadetglem2  20697  1elcpmat  20740  m2cpminv0  20786  decpmataa0  20793  monmatcollpw  20804  pmatcollpw3fi1lem1  20811  pmatcollpw3fi1lem2  20812  chfacfisf  20879  cphsubrglem  23196  mdegaddle  24054  ply1divex  24116  facth1  24144  fta1blem  24148  abvcxp  25525  lfl0sc  34891  lflsc0N  34892  baerlem3lem1  37517  frlmpwfi  38194  zrrnghm  42445  zlidlring  42456  cznrng  42483  linc0scn0  42740  linc1  42742
  Copyright terms: Public domain W3C validator