Theorem ring0cl 20327

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  ‘cfv 6521  Basecbs 17255  0_gc0g 17478  Grpcgrp 18985  Ringcrg 20293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-iota 6477  df-fun 6523  df-fv 6529  df-riota 7353  df-ov 7399  df-0g 17480  df-mgm 18684  df-sgrp 18763  df-mnd 18779  df-grp 18988  df-ring 20295

This theorem is referenced by:  dvdsr01  20430  dvdsr02  20431  irredn0  20482  isnzr2  20578  isnzr2hash  20579  ringelnzr  20583  0ring  20586  01eq0ring  20590  01eq0ringOLD  20591  zrrnghm  20596  cntzsubr  20666  domneq0r  20783  imadrhmcl  20853  abv0  20879  abvtrivd  20888  lmod0cl  20962  lmod0vs  20969  lmodvs0  20970  rhmpreimaidl  21354  lpi0  21403  frlmphllem  21839  frlmphl  21840  uvcvvcl2  21847  uvcff  21850  psr1cl  22019  mvrf  22043  mplmon  22095  mplmonmul  22096  mplcoe1  22097  evlslem3  22140  selvvvval  22202  coe1z  22333  coe1tmfv2  22345  ply1scln0  22361  ply1chr  22376  gsummoncoe1  22378  rhmmpl  22450  rhmply1vr1  22454  mamumat1cl  22506  dmatsubcl  22565  dmatmulcl  22567  scmatscmiddistr  22575  marrepcl  22631  mdetr0  22672  mdetunilem8  22686  mdetunilem9  22687  maducoeval2  22707  maduf  22708  madutpos  22709  madugsum  22710  marep01ma  22727  smadiadetlem4  22736  smadiadetglem2  22739  1elcpmat  22782  m2cpminv0  22828  decpmataa0  22835  monmatcollpw  22846  pmatcollpw3fi1lem1  22853  pmatcollpw3fi1lem2  22854  chfacfisf  22921  cphsubrglem  25246  mdegaddle  26141  ply1divex  26204  r1pid2  26229  facth1  26234  fta1blem  26238  abvcxp  27686  rloccring  33458  elrspunidl  33617  elrspunsn  33618  rhmimaidl  33621  qsidomlem2  33643  ply1degltel  33793  ply1degleel  33794  ply1degltlss  33795  gsummoncoe1fzo  33796  ply1gsumz  33798  r1p0  33805  r1pquslmic  33809  extvfvvcl  33834  psrmon  33848  psrmonmul  33849  zrhcntr  34278  lfl0sc  39711  lflsc0N  39712  baerlem3lem1  42336  ricdrng1  43151  rhmpsr  43170  evl0  43172  evlsbagval  43173  frlmpwfi  43680  mnringmulrcld  44809  zlidlring  48847  cznrng  48874  linc0scn0  49036  linc1  49038