Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ringmgp | Structured version Visualization version GIF version |
Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
Ref | Expression |
---|---|
ringmgp.g | ⊢ 𝐺 = (mulGrp‘𝑅) |
Ref | Expression |
---|---|
ringmgp | ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2818 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | ringmgp.g | . . 3 ⊢ 𝐺 = (mulGrp‘𝑅) | |
3 | eqid 2818 | . . 3 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
4 | eqid 2818 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
5 | 1, 2, 3, 4 | isring 19230 | . 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))))) |
6 | 5 | simp2bi 1138 | 1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ‘cfv 6348 (class class class)co 7145 Basecbs 16471 +gcplusg 16553 .rcmulr 16554 Mndcmnd 17899 Grpcgrp 18041 mulGrpcmgp 19168 Ringcrg 19226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-nul 5201 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-ring 19228 |
This theorem is referenced by: mgpf 19238 ringcl 19240 iscrng2 19242 ringass 19243 ringideu 19244 ringidcl 19247 ringidmlem 19249 ringsrg 19268 unitsubm 19349 dfrhm2 19398 isrhm2d 19409 idrhm 19412 pwsco1rhm 19419 pwsco2rhm 19420 subrgcrng 19468 subrgsubm 19477 issubrg3 19492 cntzsubr 19497 pwsdiagrhm 19498 subrgacs 19508 assamulgscmlem2 20057 psrcrng 20121 mplcoe3 20175 mplcoe5lem 20176 mplcoe5 20177 evlsgsummul 20233 ply1moncl 20367 coe1pwmul 20375 ply1coefsupp 20391 ply1coe 20392 gsummoncoe1 20400 lply1binomsc 20403 evls1gsummul 20416 evl1expd 20436 evl1gsummul 20451 evl1scvarpw 20454 evl1scvarpwval 20455 evl1gsummon 20456 cnfldexp 20506 expmhm 20542 nn0srg 20543 rge0srg 20544 ringvcl 20937 mat1mhm 21021 scmatmhm 21071 m1detdiag 21134 mdetdiaglem 21135 m2detleiblem2 21165 mat2pmatmhm 21269 pmatcollpwscmatlem1 21325 mply1topmatcllem 21339 mply1topmatcl 21341 pm2mpghm 21352 pm2mpmhm 21356 monmat2matmon 21360 pm2mp 21361 chpscmatgsumbin 21380 chpscmatgsummon 21381 chfacfscmulcl 21393 chfacfscmul0 21394 chfacfpmmulcl 21397 chfacfpmmul0 21398 chfacfpmmulgsum2 21401 cayhamlem1 21402 cpmadugsumlemB 21410 cpmadugsumlemC 21411 cpmadugsumlemF 21412 cayhamlem2 21420 cayhamlem4 21424 nrgtrg 23226 deg1pw 24641 plypf1 24729 efsubm 25062 amgm 25495 wilthlem2 25573 wilthlem3 25574 dchrelbas3 25741 lgsqrlem2 25850 lgsqrlem3 25851 lgsqrlem4 25852 cntrcrng 30624 psgnid 30666 cnmsgn0g 30715 altgnsg 30718 freshmansdream 30786 iistmd 31044 hbtlem4 39604 idomrootle 39673 isdomn3 39682 mon1psubm 39684 amgm2d 40429 amgm3d 40430 amgm4d 40431 c0rhm 44111 c0rnghm 44112 lidlmsgrp 44125 invginvrid 44343 ply1mulgsumlem4 44371 ply1mulgsum 44372 amgmw2d 44833 |
Copyright terms: Public domain | W3C validator |