Theorem ring0cl 20192

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  Basecbs 17171  0_gc0g 17412  Grpcgrp 18881  Ringcrg 20164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6494  df-fun 6544  df-fv 6550  df-riota 7370  df-ov 7417  df-0g 17414  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-grp 18884  df-ring 20166

This theorem is referenced by:  dvdsr01  20299  dvdsr02  20300  irredn0  20351  isnzr2  20446  isnzr2hash  20447  ringelnzr  20449  0ring  20452  01eq0ring  20456  01eq0ringOLD  20457  zrrnghm  20462  cntzsubr  20534  ringen1zr  20655  imadrhmcl  20674  abv0  20700  abvtrivd  20709  lmod0cl  20760  lmod0vs  20767  lmodvs0  20768  lpi0  21205  frlmphllem  21701  frlmphl  21702  uvcvvcl2  21709  uvcff  21712  psr1cl  21891  mvrf  21914  mplmon  21960  mplmonmul  21961  mplcoe1  21962  evlslem3  22013  coe1z  22169  coe1tmfv2  22181  ply1scl0OLD  22197  ply1scln0  22198  ply1chr  22212  gsummoncoe1  22214  mamumat1cl  22328  dmatsubcl  22387  dmatmulcl  22389  scmatscmiddistr  22397  marrepcl  22453  mdetr0  22494  mdetunilem8  22508  mdetunilem9  22509  maducoeval2  22529  maduf  22530  madutpos  22531  madugsum  22532  marep01ma  22549  smadiadetlem4  22558  smadiadetglem2  22561  1elcpmat  22604  m2cpminv0  22650  decpmataa0  22657  monmatcollpw  22668  pmatcollpw3fi1lem1  22675  pmatcollpw3fi1lem2  22676  chfacfisf  22743  cphsubrglem  25092  mdegaddle  25997  ply1divex  26059  facth1  26088  fta1blem  26092  abvcxp  27535  rhmpreimaidl  33070  elrspunidl  33079  elrspunsn  33080  rhmimaidl  33083  qsidomlem2  33105  ply1degltel  33197  ply1degleel  33198  ply1degltlss  33199  gsummoncoe1fzo  33200  ply1gsumz  33201  r1p0  33208  r1pid2  33211  r1pquslmic  33213  lfl0sc  38491  lflsc0N  38492  baerlem3lem1  41117  ricdrng1  41686  rhmmpl  41708  evl0  41712  evlsbagval  41721  selvvvval  41740  frlmpwfi  42444  mnringmulrcld  43588  zlidlring  47219  cznrng  47246  linc0scn0  47414  linc1  47416