Theorem ring0cl 20178

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 20149	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2		ring0cl.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		ring0cl.z	. . 3 ⊢ 0 = (0g‘𝑅)
4	2, 3	grpidcl 18870	. 2 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵)
5	1, 4	syl 17	1 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ‘cfv 6477  Basecbs 17112  0_gc0g 17335  Grpcgrp 18838  Ringcrg 20144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6433  df-fun 6479  df-fv 6485  df-riota 7298  df-ov 7344  df-0g 17337  df-mgm 18540  df-sgrp 18619  df-mnd 18635  df-grp 18841  df-ring 20146

This theorem is referenced by:  dvdsr01  20282  dvdsr02  20283  irredn0  20334  isnzr2  20426  isnzr2hash  20427  ringelnzr  20431  0ring  20434  01eq0ring  20438  01eq0ringOLD  20439  zrrnghm  20444  cntzsubr  20514  domneq0r  20632  ringen1zr  20686  imadrhmcl  20705  abv0  20731  abvtrivd  20740  lmod0cl  20814  lmod0vs  20821  lmodvs0  20822  rhmpreimaidl  21207  lpi0  21256  frlmphllem  21710  frlmphl  21711  uvcvvcl2  21718  uvcff  21721  psr1cl  21891  mvrf  21915  mplmon  21963  mplmonmul  21964  mplcoe1  21965  evlslem3  22008  coe1z  22170  coe1tmfv2  22182  ply1scl0OLD  22198  ply1scln0  22199  ply1chr  22214  gsummoncoe1  22216  rhmmpl  22291  rhmply1vr1  22295  mamumat1cl  22347  dmatsubcl  22406  dmatmulcl  22408  scmatscmiddistr  22416  marrepcl  22472  mdetr0  22513  mdetunilem8  22527  mdetunilem9  22528  maducoeval2  22548  maduf  22549  madutpos  22550  madugsum  22551  marep01ma  22568  smadiadetlem4  22577  smadiadetglem2  22580  1elcpmat  22623  m2cpminv0  22669  decpmataa0  22676  monmatcollpw  22687  pmatcollpw3fi1lem1  22694  pmatcollpw3fi1lem2  22695  chfacfisf  22762  cphsubrglem  25097  mdegaddle  25999  ply1divex  26062  r1pid2  26087  facth1  26092  fta1blem  26096  abvcxp  27546  rloccring  33227  elrspunidl  33383  elrspunsn  33384  rhmimaidl  33387  qsidomlem2  33408  ply1degltel  33545  ply1degleel  33546  ply1degltlss  33547  gsummoncoe1fzo  33548  ply1gsumz  33549  r1p0  33556  r1pid2OLD  33559  r1pquslmic  33561  zrhcntr  33982  lfl0sc  39100  lflsc0N  39101  baerlem3lem1  41725  ricdrng1  42540  rhmpsr  42564  evl0  42569  evlsbagval  42578  selvvvval  42597  frlmpwfi  43110  mnringmulrcld  44240  zlidlring  48244  cznrng  48271  linc0scn0  48434  linc1  48436