Theorem ring0cl 20191

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ‘cfv 6487  Basecbs 17126  0_gc0g 17349  Grpcgrp 18852  Ringcrg 20157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6443  df-fun 6489  df-fv 6495  df-riota 7309  df-ov 7355  df-0g 17351  df-mgm 18554  df-sgrp 18633  df-mnd 18649  df-grp 18855  df-ring 20159

This theorem is referenced by:  dvdsr01  20295  dvdsr02  20296  irredn0  20347  isnzr2  20439  isnzr2hash  20440  ringelnzr  20444  0ring  20447  01eq0ring  20451  01eq0ringOLD  20452  zrrnghm  20457  cntzsubr  20527  domneq0r  20645  ringen1zr  20699  imadrhmcl  20718  abv0  20744  abvtrivd  20753  lmod0cl  20827  lmod0vs  20834  lmodvs0  20835  rhmpreimaidl  21220  lpi0  21269  frlmphllem  21723  frlmphl  21724  uvcvvcl2  21731  uvcff  21734  psr1cl  21904  mvrf  21928  mplmon  21976  mplmonmul  21977  mplcoe1  21978  evlslem3  22021  coe1z  22183  coe1tmfv2  22195  ply1scl0OLD  22211  ply1scln0  22212  ply1chr  22227  gsummoncoe1  22229  rhmmpl  22304  rhmply1vr1  22308  mamumat1cl  22360  dmatsubcl  22419  dmatmulcl  22421  scmatscmiddistr  22429  marrepcl  22485  mdetr0  22526  mdetunilem8  22540  mdetunilem9  22541  maducoeval2  22561  maduf  22562  madutpos  22563  madugsum  22564  marep01ma  22581  smadiadetlem4  22590  smadiadetglem2  22593  1elcpmat  22636  m2cpminv0  22682  decpmataa0  22689  monmatcollpw  22700  pmatcollpw3fi1lem1  22707  pmatcollpw3fi1lem2  22708  chfacfisf  22775  cphsubrglem  25110  mdegaddle  26012  ply1divex  26075  r1pid2  26100  facth1  26105  fta1blem  26109  abvcxp  27559  rloccring  33244  elrspunidl  33400  elrspunsn  33401  rhmimaidl  33404  qsidomlem2  33425  ply1degltel  33562  ply1degleel  33563  ply1degltlss  33564  gsummoncoe1fzo  33565  ply1gsumz  33566  r1p0  33573  r1pid2OLD  33576  r1pquslmic  33578  zrhcntr  33999  lfl0sc  39187  lflsc0N  39188  baerlem3lem1  41812  ricdrng1  42627  rhmpsr  42651  evl0  42656  evlsbagval  42665  selvvvval  42684  frlmpwfi  43196  mnringmulrcld  44326  zlidlring  48339  cznrng  48366  linc0scn0  48529  linc1  48531