Theorem ring0cl 20290

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Basecbs 17258  0_gc0g 17499  Grpcgrp 18973  Ringcrg 20260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-ring 20262

This theorem is referenced by:  dvdsr01  20397  dvdsr02  20398  irredn0  20449  isnzr2  20544  isnzr2hash  20545  ringelnzr  20549  0ring  20552  01eq0ring  20556  01eq0ringOLD  20557  zrrnghm  20562  cntzsubr  20634  domneq0r  20746  ringen1zr  20801  imadrhmcl  20820  abv0  20846  abvtrivd  20855  lmod0cl  20908  lmod0vs  20915  lmodvs0  20916  rhmpreimaidl  21310  lpi0  21359  frlmphllem  21823  frlmphl  21824  uvcvvcl2  21831  uvcff  21834  psr1cl  22004  mvrf  22028  mplmon  22076  mplmonmul  22077  mplcoe1  22078  evlslem3  22127  coe1z  22287  coe1tmfv2  22299  ply1scl0OLD  22315  ply1scln0  22316  ply1chr  22331  gsummoncoe1  22333  rhmmpl  22408  rhmply1vr1  22412  mamumat1cl  22466  dmatsubcl  22525  dmatmulcl  22527  scmatscmiddistr  22535  marrepcl  22591  mdetr0  22632  mdetunilem8  22646  mdetunilem9  22647  maducoeval2  22667  maduf  22668  madutpos  22669  madugsum  22670  marep01ma  22687  smadiadetlem4  22696  smadiadetglem2  22699  1elcpmat  22742  m2cpminv0  22788  decpmataa0  22795  monmatcollpw  22806  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  chfacfisf  22881  cphsubrglem  25230  mdegaddle  26133  ply1divex  26196  r1pid2  26221  facth1  26226  fta1blem  26230  abvcxp  27677  rloccring  33242  elrspunidl  33421  elrspunsn  33422  rhmimaidl  33425  qsidomlem2  33446  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  gsummoncoe1fzo  33583  ply1gsumz  33584  r1p0  33591  r1pid2OLD  33594  r1pquslmic  33596  lfl0sc  39038  lflsc0N  39039  baerlem3lem1  41664  ricdrng1  42483  rhmpsr  42507  evl0  42512  evlsbagval  42521  selvvvval  42540  frlmpwfi  43055  mnringmulrcld  44197  zlidlring  47957  cznrng  47984  linc0scn0  48152  linc1  48154