Theorem ring0cl 20152

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  Basecbs 17120  0_gc0g 17343  Grpcgrp 18812  Ringcrg 20118

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-riota 7306  df-ov 7352  df-0g 17345  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-grp 18815  df-ring 20120

This theorem is referenced by:  dvdsr01  20256  dvdsr02  20257  irredn0  20308  isnzr2  20403  isnzr2hash  20404  ringelnzr  20408  0ring  20411  01eq0ring  20415  01eq0ringOLD  20416  zrrnghm  20421  cntzsubr  20491  domneq0r  20609  ringen1zr  20663  imadrhmcl  20682  abv0  20708  abvtrivd  20717  lmod0cl  20791  lmod0vs  20798  lmodvs0  20799  rhmpreimaidl  21184  lpi0  21233  frlmphllem  21687  frlmphl  21688  uvcvvcl2  21695  uvcff  21698  psr1cl  21868  mvrf  21892  mplmon  21940  mplmonmul  21941  mplcoe1  21942  evlslem3  21985  coe1z  22147  coe1tmfv2  22159  ply1scl0OLD  22175  ply1scln0  22176  ply1chr  22191  gsummoncoe1  22193  rhmmpl  22268  rhmply1vr1  22272  mamumat1cl  22324  dmatsubcl  22383  dmatmulcl  22385  scmatscmiddistr  22393  marrepcl  22449  mdetr0  22490  mdetunilem8  22504  mdetunilem9  22505  maducoeval2  22525  maduf  22526  madutpos  22527  madugsum  22528  marep01ma  22545  smadiadetlem4  22554  smadiadetglem2  22557  1elcpmat  22600  m2cpminv0  22646  decpmataa0  22653  monmatcollpw  22664  pmatcollpw3fi1lem1  22671  pmatcollpw3fi1lem2  22672  chfacfisf  22739  cphsubrglem  25075  mdegaddle  25977  ply1divex  26040  r1pid2  26065  facth1  26070  fta1blem  26074  abvcxp  27524  rloccring  33211  elrspunidl  33366  elrspunsn  33367  rhmimaidl  33370  qsidomlem2  33391  ply1degltel  33528  ply1degleel  33529  ply1degltlss  33530  gsummoncoe1fzo  33531  ply1gsumz  33532  r1p0  33539  r1pid2OLD  33542  r1pquslmic  33544  zrhcntr  33952  lfl0sc  39071  lflsc0N  39072  baerlem3lem1  41696  ricdrng1  42511  rhmpsr  42535  evl0  42540  evlsbagval  42549  selvvvval  42568  frlmpwfi  43081  mnringmulrcld  44211  zlidlring  48228  cznrng  48255  linc0scn0  48418  linc1  48420