Theorem ring0cl 20237

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6487  Basecbs 17168  0_gc0g 17391  Grpcgrp 18898  Ringcrg 20203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rmo 3340  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-iota 6443  df-fun 6489  df-fv 6495  df-riota 7313  df-ov 7359  df-0g 17393  df-mgm 18597  df-sgrp 18676  df-mnd 18692  df-grp 18901  df-ring 20205

This theorem is referenced by:  dvdsr01  20340  dvdsr02  20341  irredn0  20392  isnzr2  20484  isnzr2hash  20485  ringelnzr  20489  0ring  20492  01eq0ring  20496  01eq0ringOLD  20497  zrrnghm  20502  cntzsubr  20572  domneq0r  20690  ringen1zr  20744  imadrhmcl  20763  abv0  20789  abvtrivd  20798  lmod0cl  20872  lmod0vs  20879  lmodvs0  20880  rhmpreimaidl  21264  lpi0  21313  frlmphllem  21749  frlmphl  21750  uvcvvcl2  21757  uvcff  21760  psr1cl  21928  mvrf  21952  mplmon  22002  mplmonmul  22003  mplcoe1  22004  evlslem3  22047  coe1z  22216  coe1tmfv2  22228  ply1scln0  22244  ply1chr  22259  gsummoncoe1  22261  rhmmpl  22336  rhmply1vr1  22340  mamumat1cl  22392  dmatsubcl  22451  dmatmulcl  22453  scmatscmiddistr  22461  marrepcl  22517  mdetr0  22558  mdetunilem8  22572  mdetunilem9  22573  maducoeval2  22593  maduf  22594  madutpos  22595  madugsum  22596  marep01ma  22613  smadiadetlem4  22622  smadiadetglem2  22625  1elcpmat  22668  m2cpminv0  22714  decpmataa0  22721  monmatcollpw  22732  pmatcollpw3fi1lem1  22739  pmatcollpw3fi1lem2  22740  chfacfisf  22807  cphsubrglem  25132  mdegaddle  26027  ply1divex  26090  r1pid2  26115  facth1  26120  fta1blem  26124  abvcxp  27566  rloccring  33319  elrspunidl  33476  elrspunsn  33477  rhmimaidl  33480  qsidomlem2  33501  ply1degltel  33642  ply1degleel  33643  ply1degltlss  33644  gsummoncoe1fzo  33645  ply1gsumz  33647  r1p0  33654  r1pid2OLD  33657  r1pquslmic  33659  extvfvvcl  33667  psrmon  33681  psrmonmul  33682  zrhcntr  34111  lfl0sc  39516  lflsc0N  39517  baerlem3lem1  42141  ricdrng1  42961  rhmpsr  42983  evl0  42986  evlsbagval  42990  selvvvval  43006  frlmpwfi  43514  mnringmulrcld  44643  zlidlring  48698  cznrng  48725  linc0scn0  48887  linc1  48889