Theorem ring0cl 18956

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

Step	Hyp	Ref	Expression
1		ringgrp 18939	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2		ring0cl.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		ring0cl.z	. . 3 ⊢ 0 = (0g‘𝑅)
4	2, 3	grpidcl 17837	. 2 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵)
5	1, 4	syl 17	1 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  ‘cfv 6135  Basecbs 16255  0_gc0g 16486  Grpcgrp 17809  Ringcrg 18934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-iota 6099  df-fun 6137  df-fv 6143  df-riota 6883  df-ov 6925  df-0g 16488  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-grp 17812  df-ring 18936

This theorem is referenced by:  dvdsr01  19042  dvdsr02  19043  irredn0  19090  f1rhm0to0OLD  19130  cntzsubr  19204  abv0  19223  abvtrivd  19232  lmod0cl  19281  lmod0vs  19288  lmodvs0  19289  lpi0  19644  isnzr2  19660  isnzr2hash  19661  ringelnzr  19663  0ring  19667  01eq0ring  19669  ringen1zr  19674  psr1cl  19799  mvrf  19821  mplmon  19860  mplmonmul  19861  mplcoe1  19862  evlslem3  19910  coe1z  20029  coe1tmfv2  20041  ply1scl0  20056  ply1scln0  20057  gsummoncoe1  20070  frlmphllem  20523  frlmphl  20524  uvcvvcl2  20531  uvcff  20534  mamumat1cl  20649  dmatsubcl  20709  dmatmulcl  20711  scmatscmiddistr  20719  marrepcl  20775  mdetr0  20816  mdetunilem8  20830  mdetunilem9  20831  maducoeval2  20851  maduf  20852  madutpos  20853  madugsum  20854  marep01ma  20872  smadiadetlem4  20881  smadiadetglem2  20884  1elcpmat  20927  m2cpminv0  20973  decpmataa0  20980  monmatcollpw  20991  pmatcollpw3fi1lem1  20998  pmatcollpw3fi1lem2  20999  chfacfisf  21066  cphsubrglem  23384  mdegaddle  24271  ply1divex  24333  facth1  24361  fta1blem  24365  abvcxp  25756  lfl0sc  35238  lflsc0N  35239  baerlem3lem1  37863  frlmpwfi  38631  zrrnghm  42936  zlidlring  42947  cznrng  42974  linc0scn0  43231  linc1  43233