Theorem ring0cl 19817

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  Basecbs 16921  0_gc0g 17159  Grpcgrp 18586  Ringcrg 19792

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-riota 7241  df-ov 7287  df-0g 17161  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-grp 18589  df-ring 19794

This theorem is referenced by:  dvdsr01  19906  dvdsr02  19907  irredn0  19954  cntzsubr  20066  abv0  20100  abvtrivd  20109  lmod0cl  20158  lmod0vs  20165  lmodvs0  20166  lpi0  20527  isnzr2  20543  isnzr2hash  20544  ringelnzr  20546  0ring  20550  01eq0ring  20552  ringen1zr  20557  frlmphllem  20996  frlmphl  20997  uvcvvcl2  21004  uvcff  21007  psr1cl  21180  mvrf  21202  mplmon  21245  mplmonmul  21246  mplcoe1  21247  evlslem3  21299  coe1z  21443  coe1tmfv2  21455  ply1scl0  21470  ply1scln0  21471  gsummoncoe1  21484  mamumat1cl  21597  dmatsubcl  21656  dmatmulcl  21658  scmatscmiddistr  21666  marrepcl  21722  mdetr0  21763  mdetunilem8  21777  mdetunilem9  21778  maducoeval2  21798  maduf  21799  madutpos  21800  madugsum  21801  marep01ma  21818  smadiadetlem4  21827  smadiadetglem2  21830  1elcpmat  21873  m2cpminv0  21919  decpmataa0  21926  monmatcollpw  21937  pmatcollpw3fi1lem1  21944  pmatcollpw3fi1lem2  21945  chfacfisf  22012  cphsubrglem  24350  mdegaddle  25248  ply1divex  25310  facth1  25338  fta1blem  25342  abvcxp  26772  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  qsidomlem2  31638  ply1chr  31678  lfl0sc  37103  lflsc0N  37104  baerlem3lem1  39728  selvval2lem4  40235  evl0  40278  evlsbagval  40282  mhphf  40292  frlmpwfi  40930  mnringmulrcld  41853  zrrnghm  45486  zlidlring  45497  cznrng  45524  linc0scn0  45775  linc1  45777