Theorem ring0cl 20248

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6499  Basecbs 17179  0_gc0g 17402  Grpcgrp 18909  Ringcrg 20214

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6455  df-fun 6501  df-fv 6507  df-riota 7324  df-ov 7370  df-0g 17404  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-grp 18912  df-ring 20216

This theorem is referenced by:  dvdsr01  20351  dvdsr02  20352  irredn0  20403  isnzr2  20495  isnzr2hash  20496  ringelnzr  20500  0ring  20503  01eq0ring  20507  01eq0ringOLD  20508  zrrnghm  20513  cntzsubr  20583  domneq0r  20701  ringen1zr  20755  imadrhmcl  20774  abv0  20800  abvtrivd  20809  lmod0cl  20883  lmod0vs  20890  lmodvs0  20891  rhmpreimaidl  21275  lpi0  21324  frlmphllem  21760  frlmphl  21761  uvcvvcl2  21768  uvcff  21771  psr1cl  21939  mvrf  21963  mplmon  22013  mplmonmul  22014  mplcoe1  22015  evlslem3  22058  coe1z  22228  coe1tmfv2  22240  ply1scln0  22256  ply1chr  22271  gsummoncoe1  22273  rhmmpl  22348  rhmply1vr1  22352  mamumat1cl  22404  dmatsubcl  22463  dmatmulcl  22465  scmatscmiddistr  22473  marrepcl  22529  mdetr0  22570  mdetunilem8  22584  mdetunilem9  22585  maducoeval2  22605  maduf  22606  madutpos  22607  madugsum  22608  marep01ma  22625  smadiadetlem4  22634  smadiadetglem2  22637  1elcpmat  22680  m2cpminv0  22726  decpmataa0  22733  monmatcollpw  22744  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  chfacfisf  22819  cphsubrglem  25144  mdegaddle  26039  ply1divex  26102  r1pid2  26127  facth1  26132  fta1blem  26136  abvcxp  27578  rloccring  33331  elrspunidl  33488  elrspunsn  33489  rhmimaidl  33492  qsidomlem2  33513  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  gsummoncoe1fzo  33657  ply1gsumz  33659  r1p0  33666  r1pid2OLD  33669  r1pquslmic  33671  extvfvvcl  33679  psrmon  33693  psrmonmul  33694  zrhcntr  34123  lfl0sc  39528  lflsc0N  39529  baerlem3lem1  42153  ricdrng1  42973  rhmpsr  42995  evl0  42998  evlsbagval  43002  selvvvval  43018  frlmpwfi  43526  mnringmulrcld  44655  zlidlring  48704  cznrng  48731  linc0scn0  48893  linc1  48895