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 19302 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ring0cl.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ring0cl.z | . . 3 ⊢ 0 = (0g‘𝑅) | |
4 | 2, 3 | grpidcl 18131 | . 2 ⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 ‘cfv 6355 Basecbs 16483 0gc0g 16713 Grpcgrp 18103 Ringcrg 19297 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-iota 6314 df-fun 6357 df-fv 6363 df-riota 7114 df-ov 7159 df-0g 16715 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-grp 18106 df-ring 19299 |
This theorem is referenced by: dvdsr01 19405 dvdsr02 19406 irredn0 19453 f1rhm0to0OLD 19493 cntzsubr 19568 abv0 19602 abvtrivd 19611 lmod0cl 19660 lmod0vs 19667 lmodvs0 19668 lpi0 20020 isnzr2 20036 isnzr2hash 20037 ringelnzr 20039 0ring 20043 01eq0ring 20045 ringen1zr 20050 psr1cl 20182 mvrf 20204 mplmon 20244 mplmonmul 20245 mplcoe1 20246 evlslem3 20293 coe1z 20431 coe1tmfv2 20443 ply1scl0 20458 ply1scln0 20459 gsummoncoe1 20472 frlmphllem 20924 frlmphl 20925 uvcvvcl2 20932 uvcff 20935 mamumat1cl 21048 dmatsubcl 21107 dmatmulcl 21109 scmatscmiddistr 21117 marrepcl 21173 mdetr0 21214 mdetunilem8 21228 mdetunilem9 21229 maducoeval2 21249 maduf 21250 madutpos 21251 madugsum 21252 marep01ma 21269 smadiadetlem4 21278 smadiadetglem2 21281 1elcpmat 21323 m2cpminv0 21369 decpmataa0 21376 monmatcollpw 21387 pmatcollpw3fi1lem1 21394 pmatcollpw3fi1lem2 21395 chfacfisf 21462 cphsubrglem 23781 mdegaddle 24668 ply1divex 24730 facth1 24758 fta1blem 24762 abvcxp 26191 qsidomlem2 30966 lfl0sc 36233 lflsc0N 36234 baerlem3lem1 38858 selvval2lem4 39156 frlmpwfi 39718 zrrnghm 44208 zlidlring 44219 cznrng 44246 linc0scn0 44498 linc1 44500 |
Copyright terms: Public domain | W3C validator |