Theorem ring0cl 20227

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6531  Basecbs 17228  0_gc0g 17453  Grpcgrp 18916  Ringcrg 20193

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-riota 7362  df-ov 7408  df-0g 17455  df-mgm 18618  df-sgrp 18697  df-mnd 18713  df-grp 18919  df-ring 20195

This theorem is referenced by:  dvdsr01  20331  dvdsr02  20332  irredn0  20383  isnzr2  20478  isnzr2hash  20479  ringelnzr  20483  0ring  20486  01eq0ring  20490  01eq0ringOLD  20491  zrrnghm  20496  cntzsubr  20566  domneq0r  20684  ringen1zr  20738  imadrhmcl  20757  abv0  20783  abvtrivd  20792  lmod0cl  20845  lmod0vs  20852  lmodvs0  20853  rhmpreimaidl  21238  lpi0  21287  frlmphllem  21740  frlmphl  21741  uvcvvcl2  21748  uvcff  21751  psr1cl  21921  mvrf  21945  mplmon  21993  mplmonmul  21994  mplcoe1  21995  evlslem3  22038  coe1z  22200  coe1tmfv2  22212  ply1scl0OLD  22228  ply1scln0  22229  ply1chr  22244  gsummoncoe1  22246  rhmmpl  22321  rhmply1vr1  22325  mamumat1cl  22377  dmatsubcl  22436  dmatmulcl  22438  scmatscmiddistr  22446  marrepcl  22502  mdetr0  22543  mdetunilem8  22557  mdetunilem9  22558  maducoeval2  22578  maduf  22579  madutpos  22580  madugsum  22581  marep01ma  22598  smadiadetlem4  22607  smadiadetglem2  22610  1elcpmat  22653  m2cpminv0  22699  decpmataa0  22706  monmatcollpw  22717  pmatcollpw3fi1lem1  22724  pmatcollpw3fi1lem2  22725  chfacfisf  22792  cphsubrglem  25129  mdegaddle  26031  ply1divex  26094  r1pid2  26119  facth1  26124  fta1blem  26128  abvcxp  27578  rloccring  33265  elrspunidl  33443  elrspunsn  33444  rhmimaidl  33447  qsidomlem2  33468  ply1degltel  33604  ply1degleel  33605  ply1degltlss  33606  gsummoncoe1fzo  33607  ply1gsumz  33608  r1p0  33615  r1pid2OLD  33618  r1pquslmic  33620  zrhcntr  34010  lfl0sc  39100  lflsc0N  39101  baerlem3lem1  41726  ricdrng1  42551  rhmpsr  42575  evl0  42580  evlsbagval  42589  selvvvval  42608  frlmpwfi  43122  mnringmulrcld  44252  zlidlring  48209  cznrng  48236  linc0scn0  48399  linc1  48401