![]() |
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 2761 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | ringmgp.g | . . 3 ⊢ 𝐺 = (mulGrp‘𝑅) | |
3 | eqid 2761 | . . 3 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
4 | eqid 2761 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
5 | 1, 2, 3, 4 | isring 18772 | . 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))))) |
6 | 5 | simp2bi 1141 | 1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2140 ∀wral 3051 ‘cfv 6050 (class class class)co 6815 Basecbs 16080 +gcplusg 16164 .rcmulr 16165 Mndcmnd 17516 Grpcgrp 17644 mulGrpcmgp 18710 Ringcrg 18768 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-nul 4942 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3343 df-sbc 3578 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-nul 4060 df-if 4232 df-sn 4323 df-pr 4325 df-op 4329 df-uni 4590 df-br 4806 df-iota 6013 df-fv 6058 df-ov 6818 df-ring 18770 |
This theorem is referenced by: mgpf 18780 ringcl 18782 iscrng2 18784 ringass 18785 ringideu 18786 ringidcl 18789 ringidmlem 18791 ringsrg 18810 unitsubm 18891 dfrhm2 18940 isrhm2d 18951 idrhm 18954 pwsco1rhm 18961 pwsco2rhm 18962 subrgcrng 19007 subrgsubm 19016 issubrg3 19031 cntzsubr 19035 pwsdiagrhm 19036 assamulgscmlem2 19572 psrcrng 19636 mplcoe3 19689 mplcoe5lem 19690 mplcoe5 19691 ply1moncl 19864 coe1pwmul 19872 ply1coefsupp 19888 ply1coe 19889 gsummoncoe1 19897 lply1binomsc 19900 evls1gsummul 19913 evl1expd 19932 evl1gsummul 19947 evl1scvarpw 19950 evl1scvarpwval 19951 evl1gsummon 19952 cnfldexp 20002 expmhm 20038 nn0srg 20039 rge0srg 20040 ringvcl 20427 mat1mhm 20513 scmatmhm 20563 m1detdiag 20626 mdetdiaglem 20627 m2detleiblem2 20657 mat2pmatmhm 20761 pmatcollpwscmatlem1 20817 mply1topmatcllem 20831 mply1topmatcl 20833 pm2mpghm 20844 pm2mpmhm 20848 monmat2matmon 20852 pm2mp 20853 chpscmatgsumbin 20872 chpscmatgsummon 20873 chfacfscmulcl 20885 chfacfscmul0 20886 chfacfpmmulcl 20889 chfacfpmmul0 20890 chfacfpmmulgsum2 20893 cayhamlem1 20894 cpmadugsumlemB 20902 cpmadugsumlemC 20903 cpmadugsumlemF 20904 cayhamlem2 20912 cayhamlem4 20916 nrgtrg 22716 deg1pw 24100 plypf1 24188 efsubm 24518 amgm 24938 wilthlem2 25016 wilthlem3 25017 dchrelbas3 25184 lgsqrlem2 25293 lgsqrlem3 25294 lgsqrlem4 25295 psgnid 30178 iistmd 30279 hbtlem4 38217 subrgacs 38291 idomrootle 38294 isdomn3 38303 mon1psubm 38305 amgm2d 39022 amgm3d 39023 amgm4d 39024 c0rhm 42441 c0rnghm 42442 lidlmsgrp 42455 invginvrid 42677 ply1mulgsumlem4 42706 ply1mulgsum 42707 amgmw2d 43082 |
Copyright terms: Public domain | W3C validator |