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 2821 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | ringmgp.g | . . 3 ⊢ 𝐺 = (mulGrp‘𝑅) | |
3 | eqid 2821 | . . 3 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
4 | eqid 2821 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
5 | 1, 2, 3, 4 | isring 19232 | . 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 3138 ‘cfv 6349 (class class class)co 7145 Basecbs 16473 +gcplusg 16555 .rcmulr 16556 Mndcmnd 17901 Grpcgrp 18043 mulGrpcmgp 19170 Ringcrg 19228 |
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 2793 ax-nul 5202 |
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 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7148 df-ring 19230 |
This theorem is referenced by: mgpf 19240 ringcl 19242 iscrng2 19244 ringass 19245 ringideu 19246 ringidcl 19249 ringidmlem 19251 ringsrg 19270 unitsubm 19351 dfrhm2 19400 isrhm2d 19411 idrhm 19414 pwsco1rhm 19421 pwsco2rhm 19422 subrgcrng 19470 subrgsubm 19479 issubrg3 19494 cntzsubr 19499 pwsdiagrhm 19500 subrgacs 19510 assamulgscmlem2 20059 psrcrng 20123 mplcoe3 20177 mplcoe5lem 20178 mplcoe5 20179 evlsgsummul 20235 ply1moncl 20369 coe1pwmul 20377 ply1coefsupp 20393 ply1coe 20394 gsummoncoe1 20402 lply1binomsc 20405 evls1gsummul 20418 evl1expd 20438 evl1gsummul 20453 evl1scvarpw 20456 evl1scvarpwval 20457 evl1gsummon 20458 cnfldexp 20508 expmhm 20544 nn0srg 20545 rge0srg 20546 ringvcl 20939 mat1mhm 21023 scmatmhm 21073 m1detdiag 21136 mdetdiaglem 21137 m2detleiblem2 21167 mat2pmatmhm 21271 pmatcollpwscmatlem1 21327 mply1topmatcllem 21341 mply1topmatcl 21343 pm2mpghm 21354 pm2mpmhm 21358 monmat2matmon 21362 pm2mp 21363 chpscmatgsumbin 21382 chpscmatgsummon 21383 chfacfscmulcl 21395 chfacfscmul0 21396 chfacfpmmulcl 21399 chfacfpmmul0 21400 chfacfpmmulgsum2 21403 cayhamlem1 21404 cpmadugsumlemB 21412 cpmadugsumlemC 21413 cpmadugsumlemF 21414 cayhamlem2 21422 cayhamlem4 21426 nrgtrg 23228 deg1pw 24643 plypf1 24731 efsubm 25062 amgm 25496 wilthlem2 25574 wilthlem3 25575 dchrelbas3 25742 lgsqrlem2 25851 lgsqrlem3 25852 lgsqrlem4 25853 cntrcrng 30625 psgnid 30667 cnmsgn0g 30716 altgnsg 30719 freshmansdream 30787 iistmd 31045 hbtlem4 39606 idomrootle 39675 isdomn3 39684 mon1psubm 39686 amgm2d 40432 amgm3d 40433 amgm4d 40434 c0rhm 44081 c0rnghm 44082 lidlmsgrp 44095 invginvrid 44313 ply1mulgsumlem4 44341 ply1mulgsum 44342 amgmw2d 44803 |
Copyright terms: Public domain | W3C validator |