Theorem ring0cl 20176

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  Basecbs 17179  0_gc0g 17402  Grpcgrp 18865  Ringcrg 20142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-riota 7344  df-ov 7390  df-0g 17404  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-grp 18868  df-ring 20144

This theorem is referenced by:  dvdsr01  20280  dvdsr02  20281  irredn0  20332  isnzr2  20427  isnzr2hash  20428  ringelnzr  20432  0ring  20435  01eq0ring  20439  01eq0ringOLD  20440  zrrnghm  20445  cntzsubr  20515  domneq0r  20633  ringen1zr  20687  imadrhmcl  20706  abv0  20732  abvtrivd  20741  lmod0cl  20794  lmod0vs  20801  lmodvs0  20802  rhmpreimaidl  21187  lpi0  21236  frlmphllem  21689  frlmphl  21690  uvcvvcl2  21697  uvcff  21700  psr1cl  21870  mvrf  21894  mplmon  21942  mplmonmul  21943  mplcoe1  21944  evlslem3  21987  coe1z  22149  coe1tmfv2  22161  ply1scl0OLD  22177  ply1scln0  22178  ply1chr  22193  gsummoncoe1  22195  rhmmpl  22270  rhmply1vr1  22274  mamumat1cl  22326  dmatsubcl  22385  dmatmulcl  22387  scmatscmiddistr  22395  marrepcl  22451  mdetr0  22492  mdetunilem8  22506  mdetunilem9  22507  maducoeval2  22527  maduf  22528  madutpos  22529  madugsum  22530  marep01ma  22547  smadiadetlem4  22556  smadiadetglem2  22559  1elcpmat  22602  m2cpminv0  22648  decpmataa0  22655  monmatcollpw  22666  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  chfacfisf  22741  cphsubrglem  25077  mdegaddle  25979  ply1divex  26042  r1pid2  26067  facth1  26072  fta1blem  26076  abvcxp  27526  rloccring  33221  elrspunidl  33399  elrspunsn  33400  rhmimaidl  33403  qsidomlem2  33424  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  gsummoncoe1fzo  33563  ply1gsumz  33564  r1p0  33571  r1pid2OLD  33574  r1pquslmic  33576  zrhcntr  33969  lfl0sc  39075  lflsc0N  39076  baerlem3lem1  41701  ricdrng1  42516  rhmpsr  42540  evl0  42545  evlsbagval  42554  selvvvval  42573  frlmpwfi  43087  mnringmulrcld  44217  zlidlring  48222  cznrng  48249  linc0scn0  48412  linc1  48414