Theorem ring0cl 20004

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  Basecbs 17094  0_gc0g 17335  Grpcgrp 18762  Ringcrg 19978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-riota 7318  df-ov 7365  df-0g 17337  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-grp 18765  df-ring 19980

This theorem is referenced by:  dvdsr01  20098  dvdsr02  20099  irredn0  20148  isnzr2  20207  isnzr2hash  20208  ringelnzr  20210  0ring  20213  01eq0ring  20215  01eq0ringOLD  20216  ringen1zr  20264  cntzsubr  20305  imadrhmcl  20320  abv0  20346  abvtrivd  20355  lmod0cl  20405  lmod0vs  20412  lmodvs0  20413  lpi0  20776  frlmphllem  21223  frlmphl  21224  uvcvvcl2  21231  uvcff  21234  psr1cl  21408  mvrf  21430  mplmon  21473  mplmonmul  21474  mplcoe1  21475  evlslem3  21527  coe1z  21671  coe1tmfv2  21683  ply1scl0  21698  ply1scln0  21699  gsummoncoe1  21712  mamumat1cl  21825  dmatsubcl  21884  dmatmulcl  21886  scmatscmiddistr  21894  marrepcl  21950  mdetr0  21991  mdetunilem8  22005  mdetunilem9  22006  maducoeval2  22026  maduf  22027  madutpos  22028  madugsum  22029  marep01ma  22046  smadiadetlem4  22055  smadiadetglem2  22058  1elcpmat  22101  m2cpminv0  22147  decpmataa0  22154  monmatcollpw  22165  pmatcollpw3fi1lem1  22172  pmatcollpw3fi1lem2  22173  chfacfisf  22240  cphsubrglem  24578  mdegaddle  25476  ply1divex  25538  facth1  25566  fta1blem  25570  abvcxp  27000  rhmpreimaidl  32275  elrspunidl  32279  rhmimaidl  32282  qsidomlem2  32302  ply1chr  32360  ply1degltel  32365  ply1degltlss  32366  gsummoncoe1fzo  32367  ply1gsumz  32368  lfl0sc  37617  lflsc0N  37618  baerlem3lem1  40243  ricdrng1  40778  rhmmpl  40799  evl0  40801  evlsbagval  40806  mhphf  40829  frlmpwfi  41483  mnringmulrcld  42630  zrrnghm  46335  zlidlring  46346  cznrng  46373  linc0scn0  46624  linc1  46626