Theorem ring0cl 20280

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  Basecbs 17244  0_gc0g 17485  Grpcgrp 18963  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-riota 7387  df-ov 7433  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-ring 20252

This theorem is referenced by:  dvdsr01  20387  dvdsr02  20388  irredn0  20439  isnzr2  20534  isnzr2hash  20535  ringelnzr  20539  0ring  20542  01eq0ring  20546  01eq0ringOLD  20547  zrrnghm  20552  cntzsubr  20622  domneq0r  20740  ringen1zr  20795  imadrhmcl  20814  abv0  20840  abvtrivd  20849  lmod0cl  20902  lmod0vs  20909  lmodvs0  20910  rhmpreimaidl  21304  lpi0  21353  frlmphllem  21817  frlmphl  21818  uvcvvcl2  21825  uvcff  21828  psr1cl  21998  mvrf  22022  mplmon  22070  mplmonmul  22071  mplcoe1  22072  evlslem3  22121  coe1z  22281  coe1tmfv2  22293  ply1scl0OLD  22309  ply1scln0  22310  ply1chr  22325  gsummoncoe1  22327  rhmmpl  22402  rhmply1vr1  22406  mamumat1cl  22460  dmatsubcl  22519  dmatmulcl  22521  scmatscmiddistr  22529  marrepcl  22585  mdetr0  22626  mdetunilem8  22640  mdetunilem9  22641  maducoeval2  22661  maduf  22662  madutpos  22663  madugsum  22664  marep01ma  22681  smadiadetlem4  22690  smadiadetglem2  22693  1elcpmat  22736  m2cpminv0  22782  decpmataa0  22789  monmatcollpw  22800  pmatcollpw3fi1lem1  22807  pmatcollpw3fi1lem2  22808  chfacfisf  22875  cphsubrglem  25224  mdegaddle  26127  ply1divex  26190  r1pid2  26215  facth1  26220  fta1blem  26224  abvcxp  27673  rloccring  33256  elrspunidl  33435  elrspunsn  33436  rhmimaidl  33439  qsidomlem2  33460  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  gsummoncoe1fzo  33597  ply1gsumz  33598  r1p0  33605  r1pid2OLD  33608  r1pquslmic  33610  zrhcntr  33941  lfl0sc  39063  lflsc0N  39064  baerlem3lem1  41689  ricdrng1  42514  rhmpsr  42538  evl0  42543  evlsbagval  42552  selvvvval  42571  frlmpwfi  43086  mnringmulrcld  44223  zlidlring  48077  cznrng  48104  linc0scn0  48268  linc1  48270