Theorem ring0cl 20285

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  ‘cfv 6506  Basecbs 17217  0_gc0g 17440  Grpcgrp 18947  Ringcrg 20251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rmo 3357  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-iota 6462  df-fun 6508  df-fv 6514  df-riota 7338  df-ov 7384  df-0g 17442  df-mgm 18646  df-sgrp 18725  df-mnd 18741  df-grp 18950  df-ring 20253

This theorem is referenced by:  dvdsr01  20388  dvdsr02  20389  irredn0  20440  isnzr2  20536  isnzr2hash  20537  ringelnzr  20541  0ring  20544  01eq0ring  20548  01eq0ringOLD  20549  zrrnghm  20554  cntzsubr  20624  domneq0r  20742  ringen1zr  20796  imadrhmcl  20815  abv0  20841  abvtrivd  20850  lmod0cl  20924  lmod0vs  20931  lmodvs0  20932  rhmpreimaidl  21316  lpi0  21365  frlmphllem  21801  frlmphl  21802  uvcvvcl2  21809  uvcff  21812  psr1cl  21981  mvrf  22005  mplmon  22057  mplmonmul  22058  mplcoe1  22059  evlslem3  22102  selvvvval  22164  coe1z  22295  coe1tmfv2  22307  ply1scln0  22323  ply1chr  22338  gsummoncoe1  22340  rhmmpl  22412  rhmply1vr1  22416  mamumat1cl  22468  dmatsubcl  22527  dmatmulcl  22529  scmatscmiddistr  22537  marrepcl  22593  mdetr0  22634  mdetunilem8  22648  mdetunilem9  22649  maducoeval2  22669  maduf  22670  madutpos  22671  madugsum  22672  marep01ma  22689  smadiadetlem4  22698  smadiadetglem2  22701  1elcpmat  22744  m2cpminv0  22790  decpmataa0  22797  monmatcollpw  22808  pmatcollpw3fi1lem1  22815  pmatcollpw3fi1lem2  22816  chfacfisf  22883  cphsubrglem  25208  mdegaddle  26103  ply1divex  26166  r1pid2  26191  facth1  26196  fta1blem  26200  abvcxp  27645  rloccring  33400  elrspunidl  33560  elrspunsn  33561  rhmimaidl  33564  qsidomlem2  33585  ply1degltel  33734  ply1degleel  33735  ply1degltlss  33736  gsummoncoe1fzo  33737  ply1gsumz  33739  r1p0  33746  r1pid2OLD  33749  r1pquslmic  33751  extvfvvcl  33776  psrmon  33790  psrmonmul  33791  zrhcntr  34220  lfl0sc  39644  lflsc0N  39645  baerlem3lem1  42269  ricdrng1  43084  rhmpsr  43103  evl0  43105  evlsbagval  43106  frlmpwfi  43613  mnringmulrcld  44742  zlidlring  48794  cznrng  48821  linc0scn0  48983  linc1  48985