Theorem ring0cl 19321

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ‘cfv 6357  Basecbs 16485  0_gc0g 16715  Grpcgrp 18105  Ringcrg 19299

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fv 6365  df-riota 7116  df-ov 7161  df-0g 16717  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-grp 18108  df-ring 19301

This theorem is referenced by:  dvdsr01  19407  dvdsr02  19408  irredn0  19455  f1rhm0to0OLD  19495  cntzsubr  19570  abv0  19604  abvtrivd  19613  lmod0cl  19662  lmod0vs  19669  lmodvs0  19670  lpi0  20022  isnzr2  20038  isnzr2hash  20039  ringelnzr  20041  0ring  20045  01eq0ring  20047  ringen1zr  20052  psr1cl  20184  mvrf  20206  mplmon  20246  mplmonmul  20247  mplcoe1  20248  evlslem3  20295  coe1z  20433  coe1tmfv2  20445  ply1scl0  20460  ply1scln0  20461  gsummoncoe1  20474  frlmphllem  20926  frlmphl  20927  uvcvvcl2  20934  uvcff  20937  mamumat1cl  21050  dmatsubcl  21109  dmatmulcl  21111  scmatscmiddistr  21119  marrepcl  21175  mdetr0  21216  mdetunilem8  21230  mdetunilem9  21231  maducoeval2  21251  maduf  21252  madutpos  21253  madugsum  21254  marep01ma  21271  smadiadetlem4  21280  smadiadetglem2  21283  1elcpmat  21325  m2cpminv0  21371  decpmataa0  21378  monmatcollpw  21389  pmatcollpw3fi1lem1  21396  pmatcollpw3fi1lem2  21397  chfacfisf  21464  cphsubrglem  23783  mdegaddle  24670  ply1divex  24732  facth1  24760  fta1blem  24764  abvcxp  26193  qsidomlem2  30968  lfl0sc  36220  lflsc0N  36221  baerlem3lem1  38845  selvval2lem4  39143  frlmpwfi  39705  zrrnghm  44195  zlidlring  44206  cznrng  44233  linc0scn0  44485  linc1  44487