Theorem ring0cl 20357

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  Basecbs 17275  0_gc0g 17498  Grpcgrp 19006  Ringcrg 20321

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-iota 6492  df-fun 6538  df-fv 6544  df-riota 7369  df-ov 7415  df-0g 17500  df-mgm 18704  df-sgrp 18783  df-mnd 18799  df-grp 19009  df-ring 20323

This theorem is used by:  dvdsr01  20460  dvdsr02  20461  irredn0  20512  isnzr2  20626  isnzr2hash  20628  ringelnzr  20632  0ring  20635  01eq0ring  20639  01eq0ringOLD  20640  zrrnghm  20646  cntzsubr  20716  domneq0r  20833  imadrhmcl  20911  abv0  20937  abvtrivd  20946  lmod0cl  21020  lmod0vs  21027  lmodvs0  21028  rhmpreimaidl  21427  qsidomlem2  21492  lpi0  21505  frlmphllem  21941  frlmphl  21942  uvcvvcl2  21949  uvcff  21952  psr1cl  22121  mvrf  22145  mplmon  22197  mplmonmul  22198  mplcoe1  22199  evlslem3  22242  selvvvval  22304  coe1z  22435  coe1tmfv2  22447  ply1scln0  22463  ply1chr  22477  gsummoncoe1  22479  rhmmpl  22551  rhmply1vr1  22555  mamumat1cl  22607  dmatsubcl  22666  dmatmulcl  22668  scmatscmiddistr  22676  marrepcl  22732  mdetr0  22773  mdetunilem8  22787  mdetunilem9  22788  maducoeval2  22808  maduf  22809  madutpos  22810  madugsum  22811  marep01ma  22828  smadiadetlem4  22837  smadiadetglem2  22840  1elcpmat  22883  m2cpminv0  22929  decpmataa0  22936  monmatcollpw  22947  pmatcollpw3fi1lem1  22954  pmatcollpw3fi1lem2  22955  chfacfisf  23022  cphsubrglem  25347  mdegaddle  26242  ply1divex  26305  r1pid2  26330  facth1  26335  fta1blem  26339  abvcxp  27790  rloccring  33600  elrspunidl  33745  elrspunsn  33746  rhmimaidl  33749  ply1degltel  33893  ply1degleel  33894  ply1degltlss  33895  gsummoncoe1fzo  33896  ply1gsumz  33898  r1p0  33905  r1pquslmic  33909  extvfvvcl  33934  psrmon  33948  psrmonmul  33949  zrhcntr  34378  lfl0sc  39884  lflsc0N  39885  baerlem3lem1  42509  ricdrng1  43324  rhmpsr  43343  evl0  43345  evlsbagval  43346  frlmpwfi  43853  mnringmulrcld  44980  zlidlring  49027  cznrng  49054  isidom3  49138  linc0scn0  49231  linc1  49233