Theorem ring0cl 20412

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Basecbs 17305  0_gc0g 17528  Grpcgrp 19061  Ringcrg 20376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-riota 7373  df-ov 7419  df-0g 17530  df-mgm 18734  df-sgrp 18825  df-mnd 18841  df-grp 19064  df-ring 20378

This theorem is used by:  dvdsr01  20516  dvdsr02  20517  irredn0  20568  isnzr2  20682  isnzr2hash  20684  ringelnzr  20688  0ring  20691  01eq0ring  20695  01eq0ringOLD  20696  zrrnghm  20702  cntzsubr  20772  domneq0r  20889  imadrhmcl  20967  abv0  20993  abvtrivd  21002  lmod0cl  21076  lmod0vs  21083  lmodvs0  21084  rhmpreimaidl  21483  qsidomlem2  21548  lpi0  21561  frlmphllem  21997  frlmphl  21998  uvcvvcl2  22005  uvcff  22008  psr1cl  22179  mvrf  22203  mplmon  22255  mplmonmul  22256  mplcoe1  22257  evlslem3  22300  selvvvval  22362  coe1z  22493  coe1tmfv2  22505  ply1scln0  22521  ply1chr  22535  gsummoncoe1  22537  rhmmpl  22609  rhmply1vr1  22613  mamumat1cl  22665  dmatsubcl  22724  dmatmulcl  22726  scmatscmiddistr  22734  marrepcl  22790  mdetr0  22831  mdetunilem8  22845  mdetunilem9  22846  maducoeval2  22866  maduf  22867  madutpos  22868  madugsum  22869  marep01ma  22886  smadiadetlem4  22895  smadiadetglem2  22898  1elcpmat  22944  m2cpminv0  22990  decpmataa0  22997  monmatcollpw  23008  pmatcollpw3fi1lem1  23015  pmatcollpw3fi1lem2  23016  chfacfisf  23083  cphsubrglem  25409  mdegaddle  26304  ply1divex  26367  r1pid2  26392  facth1  26397  fta1blem  26401  abvcxp  27852  rloccring  33713  elrspunidl  33858  elrspunsn  33859  rhmimaidl  33862  ply1degltel  34006  ply1degleel  34007  ply1degltlss  34008  gsummoncoe1fzo  34009  ply1gsumz  34011  r1p0  34018  r1pquslmic  34022  extvfvvcl  34047  psrmon  34061  psrmonmul  34062  zrhcntr  34491  lfl0sc  39957  lflsc0N  39958  baerlem3lem1  42582  ricdrng1  43412  rhmpsr  43431  evl0  43433  evlsbagval  43434  frlmpwfi  43941  mnringmulrcld  45068  zlidlring  49151  cznrng  49178  isidom3  49262  linc0scn0  49355  linc1  49357