Theorem ring0cl 20206

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  Basecbs 17137  0_gc0g 17360  Grpcgrp 18867  Ringcrg 20172

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 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-riota 7315  df-ov 7361  df-0g 17362  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-grp 18870  df-ring 20174

This theorem is referenced by:  dvdsr01  20309  dvdsr02  20310  irredn0  20361  isnzr2  20453  isnzr2hash  20454  ringelnzr  20458  0ring  20461  01eq0ring  20465  01eq0ringOLD  20466  zrrnghm  20471  cntzsubr  20541  domneq0r  20659  ringen1zr  20713  imadrhmcl  20732  abv0  20758  abvtrivd  20767  lmod0cl  20841  lmod0vs  20848  lmodvs0  20849  rhmpreimaidl  21234  lpi0  21283  frlmphllem  21737  frlmphl  21738  uvcvvcl2  21745  uvcff  21748  psr1cl  21917  mvrf  21941  mplmon  21991  mplmonmul  21992  mplcoe1  21993  evlslem3  22036  coe1z  22206  coe1tmfv2  22218  ply1scln0  22234  ply1chr  22249  gsummoncoe1  22251  rhmmpl  22326  rhmply1vr1  22330  mamumat1cl  22382  dmatsubcl  22441  dmatmulcl  22443  scmatscmiddistr  22451  marrepcl  22507  mdetr0  22548  mdetunilem8  22562  mdetunilem9  22563  maducoeval2  22583  maduf  22584  madutpos  22585  madugsum  22586  marep01ma  22603  smadiadetlem4  22612  smadiadetglem2  22615  1elcpmat  22658  m2cpminv0  22704  decpmataa0  22711  monmatcollpw  22722  pmatcollpw3fi1lem1  22729  pmatcollpw3fi1lem2  22730  chfacfisf  22797  cphsubrglem  25122  mdegaddle  26020  ply1divex  26083  r1pid2  26108  facth1  26113  fta1blem  26117  abvcxp  27566  rloccring  33336  elrspunidl  33493  elrspunsn  33494  rhmimaidl  33497  qsidomlem2  33518  ply1degltel  33659  ply1degleel  33660  ply1degltlss  33661  gsummoncoe1fzo  33662  ply1gsumz  33664  r1p0  33671  r1pid2OLD  33674  r1pquslmic  33676  extvfvvcl  33684  psrmon  33698  psrmonmul  33699  zrhcntr  34129  lfl0sc  39519  lflsc0N  39520  baerlem3lem1  42144  ricdrng1  42972  rhmpsr  42994  evl0  42997  evlsbagval  43001  selvvvval  43017  frlmpwfi  43529  mnringmulrcld  44658  zlidlring  48668  cznrng  48695  linc0scn0  48857  linc1  48859