Theorem ring0cl 20411

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  Basecbs 17304  0_gc0g 17527  Grpcgrp 19060  Ringcrg 20375

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 5251  ax-nul 5263  ax-pr 5398

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 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-riota 7371  df-ov 7417  df-0g 17529  df-mgm 18733  df-sgrp 18824  df-mnd 18840  df-grp 19063  df-ring 20377

This theorem is used by:  dvdsr01  20515  dvdsr02  20516  irredn0  20567  isnzr2  20681  isnzr2hash  20683  ringelnzr  20687  0ring  20690  01eq0ring  20694  01eq0ringOLD  20695  zrrnghm  20701  cntzsubr  20771  domneq0r  20888  imadrhmcl  20966  abv0  20992  abvtrivd  21001  lmod0cl  21075  lmod0vs  21082  lmodvs0  21083  rhmpreimaidl  21482  qsidomlem2  21547  lpi0  21560  frlmphllem  21996  frlmphl  21997  uvcvvcl2  22004  uvcff  22007  psr1cl  22178  mvrf  22202  mplmon  22254  mplmonmul  22255  mplcoe1  22256  evlslem3  22299  selvvvval  22361  coe1z  22492  coe1tmfv2  22504  ply1scln0  22520  ply1chr  22534  gsummoncoe1  22536  rhmmpl  22608  rhmply1vr1  22612  mamumat1cl  22664  dmatsubcl  22723  dmatmulcl  22725  scmatscmiddistr  22733  marrepcl  22789  mdetr0  22830  mdetunilem8  22844  mdetunilem9  22845  maducoeval2  22865  maduf  22866  madutpos  22867  madugsum  22868  marep01ma  22885  smadiadetlem4  22894  smadiadetglem2  22897  1elcpmat  22943  m2cpminv0  22989  decpmataa0  22996  monmatcollpw  23007  pmatcollpw3fi1lem1  23014  pmatcollpw3fi1lem2  23015  chfacfisf  23082  cphsubrglem  25408  mdegaddle  26302  ply1divex  26365  r1pid2  26390  facth1  26395  fta1blem  26399  abvcxp  27854  rloccring  33714  elrspunidl  33859  elrspunsn  33860  rhmimaidl  33863  ply1degltel  34007  ply1degleel  34008  ply1degltlss  34009  gsummoncoe1fzo  34010  ply1gsumz  34012  r1p0  34019  r1pquslmic  34023  extvfvvcl  34048  psrmon  34062  psrmonmul  34063  zrhcntr  34492  lfl0sc  39958  lflsc0N  39959  baerlem3lem1  42583  ricdrng1  43413  rhmpsr  43432  evl0  43434  evlsbagval  43435  frlmpwfi  43942  mnringmulrcld  45069  zlidlring  49152  cznrng  49179  isidom3  49263  linc0scn0  49356  linc1  49358