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

Theorem ring0cl 18334
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 18317 . 2 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2 ring0cl.b . . 3 𝐵 = (Base‘𝑅)
3 ring0cl.z . . 3 0 = (0g𝑅)
42, 3grpidcl 17215 . 2 (𝑅 ∈ Grp → 0𝐵)
51, 4syl 17 1 (𝑅 ∈ Ring → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  cfv 5786  Basecbs 15637  0gc0g 15865  Grpcgrp 17187  Ringcrg 18312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-iota 5750  df-fun 5788  df-fv 5794  df-riota 6485  df-ov 6526  df-0g 15867  df-mgm 17007  df-sgrp 17049  df-mnd 17060  df-grp 17190  df-ring 18314
This theorem is referenced by:  dvdsr01  18420  dvdsr02  18421  irredn0  18468  f1rhm0to0  18505  cntzsubr  18577  abv0  18596  abvtrivd  18605  lmod0cl  18654  lmod0vs  18661  lmodvs0  18662  lpi0  19010  isnzr2  19026  isnzr2hash  19027  ringelnzr  19029  0ring  19033  01eq0ring  19035  ringen1zr  19040  psr1cl  19165  mvrf  19187  mplmon  19226  mplmonmul  19227  mplcoe1  19228  evlslem3  19277  coe1z  19396  coe1tmfv2  19408  ply1scl0  19423  ply1scln0  19424  gsummoncoe1  19437  frlmphllem  19876  frlmphl  19877  uvcvvcl2  19884  uvcff  19887  mamumat1cl  20002  dmatsubcl  20061  dmatmulcl  20063  scmatscmiddistr  20071  marrepcl  20127  mdetr0  20168  mdetunilem8  20182  mdetunilem9  20183  maducoeval2  20203  maduf  20204  madutpos  20205  madugsum  20206  marep01ma  20223  smadiadetlem4  20232  smadiadetglem2  20235  1elcpmat  20277  m2cpminv0  20323  decpmataa0  20330  monmatcollpw  20341  pmatcollpw3fi1lem1  20348  pmatcollpw3fi1lem2  20349  chfacfisf  20416  cphsubrglem  22705  mdegaddle  23551  ply1divex  23613  facth1  23641  fta1blem  23645  abvcxp  25017  lfl0sc  33186  lflsc0N  33187  baerlem3lem1  35813  frlmpwfi  36485  zrrnghm  41705  zlidlring  41716  cznrng  41745  linc0scn0  42004  linc1  42006
  Copyright terms: Public domain W3C validator