![]() |
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 19955 | . 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
2 | ring0cl.b | . . 3 ⊢ 𝐵 = (Base‘𝑅) | |
3 | ring0cl.z | . . 3 ⊢ 0 = (0g‘𝑅) | |
4 | 2, 3 | grpidcl 18770 | . 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 6493 Basecbs 17075 0gc0g 17313 Grpcgrp 18740 Ringcrg 19950 |
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 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6445 df-fun 6495 df-fv 6501 df-riota 7309 df-ov 7356 df-0g 17315 df-mgm 18489 df-sgrp 18538 df-mnd 18549 df-grp 18743 df-ring 19952 |
This theorem is referenced by: dvdsr01 20069 dvdsr02 20070 irredn0 20117 cntzsubr 20240 abv0 20275 abvtrivd 20284 lmod0cl 20333 lmod0vs 20340 lmodvs0 20341 lpi0 20702 isnzr2 20718 isnzr2hash 20719 ringelnzr 20721 0ring 20725 01eq0ring 20727 ringen1zr 20732 frlmphllem 21171 frlmphl 21172 uvcvvcl2 21179 uvcff 21182 psr1cl 21355 mvrf 21377 mplmon 21420 mplmonmul 21421 mplcoe1 21422 evlslem3 21474 coe1z 21618 coe1tmfv2 21630 ply1scl0 21645 ply1scln0 21646 gsummoncoe1 21659 mamumat1cl 21772 dmatsubcl 21831 dmatmulcl 21833 scmatscmiddistr 21841 marrepcl 21897 mdetr0 21938 mdetunilem8 21952 mdetunilem9 21953 maducoeval2 21973 maduf 21974 madutpos 21975 madugsum 21976 marep01ma 21993 smadiadetlem4 22002 smadiadetglem2 22005 1elcpmat 22048 m2cpminv0 22094 decpmataa0 22101 monmatcollpw 22112 pmatcollpw3fi1lem1 22119 pmatcollpw3fi1lem2 22120 chfacfisf 22187 cphsubrglem 24525 mdegaddle 25423 ply1divex 25485 facth1 25513 fta1blem 25517 abvcxp 26947 rhmpreimaidl 32079 elrspunidl 32082 rhmimaidl 32085 qsidomlem2 32105 ply1chr 32159 lfl0sc 37511 lflsc0N 37512 baerlem3lem1 40137 selvval2lem4 40644 evl0 40695 evlsbagval 40699 mhphf 40709 frlmpwfi 41363 mnringmulrcld 42450 zrrnghm 46147 zlidlring 46158 cznrng 46185 linc0scn0 46436 linc1 46438 |
Copyright terms: Public domain | W3C validator |