![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ring0cl | Structured version Visualization version GIF version |
Description: The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
Ref | Expression |
---|---|
ring0cl.b | ⊢ 𝐵 = (Base‘𝑅) |
ring0cl.z | ⊢ 0 = (0g‘𝑅) |
Ref | Expression |
---|---|
ring0cl | ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringgrp 19983 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ring0cl.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ring0cl.z | . . 3 ⊢ 0 = (0g‘𝑅) | |
4 | 2, 3 | grpidcl 18792 | . 2 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ‘cfv 6501 Basecbs 17094 0gc0g 17335 Grpcgrp 18762 Ringcrg 19978 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-iota 6453 df-fun 6503 df-fv 6509 df-riota 7318 df-ov 7365 df-0g 17337 df-mgm 18511 df-sgrp 18560 df-mnd 18571 df-grp 18765 df-ring 19980 |
This theorem is referenced by: dvdsr01 20098 dvdsr02 20099 irredn0 20148 isnzr2 20207 isnzr2hash 20208 ringelnzr 20210 0ring 20213 01eq0ring 20215 01eq0ringOLD 20216 ringen1zr 20264 cntzsubr 20305 imadrhmcl 20320 abv0 20346 abvtrivd 20355 lmod0cl 20405 lmod0vs 20412 lmodvs0 20413 lpi0 20776 frlmphllem 21223 frlmphl 21224 uvcvvcl2 21231 uvcff 21234 psr1cl 21408 mvrf 21430 mplmon 21473 mplmonmul 21474 mplcoe1 21475 evlslem3 21527 coe1z 21671 coe1tmfv2 21683 ply1scl0 21698 ply1scln0 21699 gsummoncoe1 21712 mamumat1cl 21825 dmatsubcl 21884 dmatmulcl 21886 scmatscmiddistr 21894 marrepcl 21950 mdetr0 21991 mdetunilem8 22005 mdetunilem9 22006 maducoeval2 22026 maduf 22027 madutpos 22028 madugsum 22029 marep01ma 22046 smadiadetlem4 22055 smadiadetglem2 22058 1elcpmat 22101 m2cpminv0 22147 decpmataa0 22154 monmatcollpw 22165 pmatcollpw3fi1lem1 22172 pmatcollpw3fi1lem2 22173 chfacfisf 22240 cphsubrglem 24578 mdegaddle 25476 ply1divex 25538 facth1 25566 fta1blem 25570 abvcxp 27000 rhmpreimaidl 32275 elrspunidl 32279 rhmimaidl 32282 qsidomlem2 32302 ply1chr 32360 ply1degltel 32365 ply1degltlss 32366 gsummoncoe1fzo 32367 ply1gsumz 32368 lfl0sc 37617 lflsc0N 37618 baerlem3lem1 40243 ricdrng1 40778 rhmmpl 40799 evl0 40801 evlsbagval 40806 mhphf 40829 frlmpwfi 41483 mnringmulrcld 42630 zrrnghm 46335 zlidlring 46346 cznrng 46373 linc0scn0 46624 linc1 46626 |
Copyright terms: Public domain | W3C validator |