Theorem ring0cl 20264

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  Basecbs 17247  0_gc0g 17484  Grpcgrp 18951  Ringcrg 20230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-riota 7388  df-ov 7434  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-ring 20232

This theorem is referenced by:  dvdsr01  20371  dvdsr02  20372  irredn0  20423  isnzr2  20518  isnzr2hash  20519  ringelnzr  20523  0ring  20526  01eq0ring  20530  01eq0ringOLD  20531  zrrnghm  20536  cntzsubr  20606  domneq0r  20724  ringen1zr  20779  imadrhmcl  20798  abv0  20824  abvtrivd  20833  lmod0cl  20886  lmod0vs  20893  lmodvs0  20894  rhmpreimaidl  21287  lpi0  21336  frlmphllem  21800  frlmphl  21801  uvcvvcl2  21808  uvcff  21811  psr1cl  21981  mvrf  22005  mplmon  22053  mplmonmul  22054  mplcoe1  22055  evlslem3  22104  coe1z  22266  coe1tmfv2  22278  ply1scl0OLD  22294  ply1scln0  22295  ply1chr  22310  gsummoncoe1  22312  rhmmpl  22387  rhmply1vr1  22391  mamumat1cl  22445  dmatsubcl  22504  dmatmulcl  22506  scmatscmiddistr  22514  marrepcl  22570  mdetr0  22611  mdetunilem8  22625  mdetunilem9  22626  maducoeval2  22646  maduf  22647  madutpos  22648  madugsum  22649  marep01ma  22666  smadiadetlem4  22675  smadiadetglem2  22678  1elcpmat  22721  m2cpminv0  22767  decpmataa0  22774  monmatcollpw  22785  pmatcollpw3fi1lem1  22792  pmatcollpw3fi1lem2  22793  chfacfisf  22860  cphsubrglem  25211  mdegaddle  26113  ply1divex  26176  r1pid2  26201  facth1  26206  fta1blem  26210  abvcxp  27659  rloccring  33274  elrspunidl  33456  elrspunsn  33457  rhmimaidl  33460  qsidomlem2  33481  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  gsummoncoe1fzo  33618  ply1gsumz  33619  r1p0  33626  r1pid2OLD  33629  r1pquslmic  33631  zrhcntr  33980  lfl0sc  39083  lflsc0N  39084  baerlem3lem1  41709  ricdrng1  42538  rhmpsr  42562  evl0  42567  evlsbagval  42576  selvvvval  42595  frlmpwfi  43110  mnringmulrcld  44247  zlidlring  48150  cznrng  48177  linc0scn0  48340  linc1  48342