Theorem ring0cl 20084

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ‘cfv 6544  Basecbs 17144  0_gc0g 17385  Grpcgrp 18819  Ringcrg 20056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-riota 7365  df-ov 7412  df-0g 17387  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-ring 20058

This theorem is referenced by:  dvdsr01  20185  dvdsr02  20186  irredn0  20237  isnzr2  20297  isnzr2hash  20298  ringelnzr  20300  0ring  20303  01eq0ring  20305  01eq0ringOLD  20306  cntzsubr  20353  ringen1zr  20399  imadrhmcl  20413  abv0  20439  abvtrivd  20448  lmod0cl  20498  lmod0vs  20505  lmodvs0  20506  lpi0  20885  frlmphllem  21335  frlmphl  21336  uvcvvcl2  21343  uvcff  21346  psr1cl  21522  mvrf  21544  mplmon  21590  mplmonmul  21591  mplcoe1  21592  evlslem3  21643  coe1z  21785  coe1tmfv2  21797  ply1scl0OLD  21813  ply1scln0  21814  gsummoncoe1  21828  mamumat1cl  21941  dmatsubcl  22000  dmatmulcl  22002  scmatscmiddistr  22010  marrepcl  22066  mdetr0  22107  mdetunilem8  22121  mdetunilem9  22122  maducoeval2  22142  maduf  22143  madutpos  22144  madugsum  22145  marep01ma  22162  smadiadetlem4  22171  smadiadetglem2  22174  1elcpmat  22217  m2cpminv0  22263  decpmataa0  22270  monmatcollpw  22281  pmatcollpw3fi1lem1  22288  pmatcollpw3fi1lem2  22289  chfacfisf  22356  cphsubrglem  24694  mdegaddle  25592  ply1divex  25654  facth1  25682  fta1blem  25686  abvcxp  27118  rhmpreimaidl  32537  elrspunidl  32546  elrspunsn  32547  rhmimaidl  32550  qsidomlem2  32572  ply1chr  32661  ply1degltel  32666  ply1degltlss  32667  gsummoncoe1fzo  32668  ply1gsumz  32669  lfl0sc  37952  lflsc0N  37953  baerlem3lem1  40578  ricdrng1  41102  rhmmpl  41125  evl0  41129  evlsbagval  41138  selvvvval  41157  frlmpwfi  41840  mnringmulrcld  42987  zrrnghm  46716  zlidlring  46826  cznrng  46853  linc0scn0  47104  linc1  47106