Theorem ring0cl 20458

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  Basecbs 17349  0_gc0g 17572  Grpcgrp 19106  Ringcrg 20421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6483  df-fun 6529  df-fv 6535  df-riota 7365  df-ov 7411  df-0g 17574  df-mgm 18778  df-sgrp 18870  df-mnd 18886  df-grp 19109  df-ring 20423

This theorem is used by:  dvdsr01  20563  dvdsr02  20564  irredn0  20615  isnzr2  20730  isnzr2hash  20732  ringelnzr  20736  0ring  20739  01eq0ring  20743  01eq0ringOLD  20744  zrrnghm  20750  cntzsubr  20820  domneq0r  20937  imadrhmcl  21016  abv0  21042  abvtrivd  21051  lmod0cl  21125  lmod0vs  21132  lmodvs0  21133  rhmpreimaidl  21533  qsidomlem2  21599  lpi0  21612  frlmphllem  22048  frlmphl  22049  uvcvvcl2  22056  uvcff  22059  psr1cl  22230  mvrf  22254  mplmon  22306  mplmonmul  22307  mplcoe1  22308  evlslem3  22351  selvvvval  22413  coe1z  22544  coe1tmfv2  22556  ply1scln0  22572  ply1chr  22586  gsummoncoe1  22588  rhmmpl  22660  rhmply1vr1  22664  mamumat1cl  22716  dmatsubcl  22775  dmatmulcl  22777  scmatscmiddistr  22785  marrepcl  22841  mdetr0  22882  mdetunilem8  22896  mdetunilem9  22897  maducoeval2  22917  maduf  22918  madutpos  22919  madugsum  22920  marep01ma  22937  smadiadetlem4  22946  smadiadetglem2  22949  1elcpmat  22995  m2cpminv0  23041  decpmataa0  23048  monmatcollpw  23059  pmatcollpw3fi1lem1  23066  pmatcollpw3fi1lem2  23067  chfacfisf  23134  cphsubrglem  25460  mdegaddle  26354  ply1divex  26417  r1pid2  26442  facth1  26447  fta1blem  26451  abvcxp  27906  rloccring  33766  elrspunidl  33912  elrspunsn  33913  rhmimaidl  33916  ply1degltel  34060  ply1degleel  34061  ply1degltlss  34062  gsummoncoe1fzo  34063  ply1gsumz  34065  r1p0  34072  r1pquslmic  34076  extvfvvcl  34101  psrmon  34115  psrmonmul  34116  zrhcntr  34545  lfl0sc  40059  lflsc0N  40060  baerlem3lem1  42684  ricdrng1  43514  rhmpsr  43533  evl0  43535  evlsbagval  43536  frlmpwfi  44043  mnringmulrcld  45170  zlidlring  49253  cznrng  49280  isidom3  49364  linc0scn0  49457  linc1  49459