![]() |
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 18939 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ring0cl.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ring0cl.z | . . 3 ⊢ 0 = (0g‘𝑅) | |
4 | 2, 3 | grpidcl 17837 | . 2 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ‘cfv 6135 Basecbs 16255 0gc0g 16486 Grpcgrp 17809 Ringcrg 18934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-iota 6099 df-fun 6137 df-fv 6143 df-riota 6883 df-ov 6925 df-0g 16488 df-mgm 17628 df-sgrp 17670 df-mnd 17681 df-grp 17812 df-ring 18936 |
This theorem is referenced by: dvdsr01 19042 dvdsr02 19043 irredn0 19090 f1rhm0to0OLD 19130 cntzsubr 19204 abv0 19223 abvtrivd 19232 lmod0cl 19281 lmod0vs 19288 lmodvs0 19289 lpi0 19644 isnzr2 19660 isnzr2hash 19661 ringelnzr 19663 0ring 19667 01eq0ring 19669 ringen1zr 19674 psr1cl 19799 mvrf 19821 mplmon 19860 mplmonmul 19861 mplcoe1 19862 evlslem3 19910 coe1z 20029 coe1tmfv2 20041 ply1scl0 20056 ply1scln0 20057 gsummoncoe1 20070 frlmphllem 20523 frlmphl 20524 uvcvvcl2 20531 uvcff 20534 mamumat1cl 20649 dmatsubcl 20709 dmatmulcl 20711 scmatscmiddistr 20719 marrepcl 20775 mdetr0 20816 mdetunilem8 20830 mdetunilem9 20831 maducoeval2 20851 maduf 20852 madutpos 20853 madugsum 20854 marep01ma 20872 smadiadetlem4 20881 smadiadetglem2 20884 1elcpmat 20927 m2cpminv0 20973 decpmataa0 20980 monmatcollpw 20991 pmatcollpw3fi1lem1 20998 pmatcollpw3fi1lem2 20999 chfacfisf 21066 cphsubrglem 23384 mdegaddle 24271 ply1divex 24333 facth1 24361 fta1blem 24365 abvcxp 25756 lfl0sc 35238 lflsc0N 35239 baerlem3lem1 37863 frlmpwfi 38631 zrrnghm 42936 zlidlring 42947 cznrng 42974 linc0scn0 43231 linc1 43233 |
Copyright terms: Public domain | W3C validator |