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 2739 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
2 | ringmgp.g | . . 3 ⊢ 𝐺 = (mulGrp‘𝑅) | |
3 | eqid 2739 | . . 3 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
4 | eqid 2739 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
5 | 1, 2, 3, 4 | isring 19599 | . 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))))) |
6 | 5 | simp2bi 1148 | 1 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2112 ∀wral 3064 ‘cfv 6401 (class class class)co 7235 Basecbs 16793 +gcplusg 16835 .rcmulr 16836 Mndcmnd 18206 Grpcgrp 18398 mulGrpcmgp 19537 Ringcrg 19595 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-nul 5216 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4255 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-iota 6359 df-fv 6409 df-ov 7238 df-ring 19597 |
This theorem is referenced by: mgpf 19610 ringcl 19612 iscrng2 19614 ringass 19615 ringideu 19616 ringidcl 19619 ringidmlem 19621 ringsrg 19640 unitsubm 19721 dfrhm2 19770 isrhm2d 19781 idrhm 19784 pwsco1rhm 19791 pwsco2rhm 19792 subrgcrng 19837 subrgsubm 19846 issubrg3 19861 cntzsubr 19866 pwsdiagrhm 19867 subrgacs 19877 cnfldexp 20429 expmhm 20465 nn0srg 20466 rge0srg 20467 assamulgscmlem2 20892 psrcrng 20970 mplcoe3 21027 mplcoe5lem 21028 mplcoe5 21029 evlsgsummul 21084 mhppwdeg 21122 ply1moncl 21224 coe1pwmul 21232 ply1coefsupp 21248 ply1coe 21249 gsummoncoe1 21257 lply1binomsc 21260 evls1gsummul 21273 evl1expd 21293 evl1gsummul 21308 evl1scvarpw 21311 evl1scvarpwval 21312 evl1gsummon 21313 ringvcl 21329 mat1mhm 21413 scmatmhm 21463 m1detdiag 21526 mdetdiaglem 21527 m2detleiblem2 21557 mat2pmatmhm 21662 pmatcollpwscmatlem1 21718 mply1topmatcllem 21732 mply1topmatcl 21734 pm2mpghm 21745 pm2mpmhm 21749 monmat2matmon 21753 pm2mp 21754 chpscmatgsumbin 21773 chpscmatgsummon 21774 chfacfscmulcl 21786 chfacfscmul0 21787 chfacfpmmulcl 21790 chfacfpmmul0 21791 chfacfpmmulgsum2 21794 cayhamlem1 21795 cpmadugsumlemB 21803 cpmadugsumlemC 21804 cpmadugsumlemF 21805 cayhamlem2 21813 cayhamlem4 21817 nrgtrg 23620 deg1pw 25050 plypf1 25138 efsubm 25472 amgm 25905 wilthlem2 25983 wilthlem3 25984 dchrelbas3 26151 lgsqrlem2 26260 lgsqrlem3 26261 lgsqrlem4 26262 cntrcrng 31073 psgnid 31115 cnmsgn0g 31164 altgnsg 31167 freshmansdream 31235 frobrhm 31236 znfermltl 31308 ringlsmss 31329 iistmd 31598 pwspjmhmmgpd 40028 pwsexpg 40029 evlsbagval 40034 evlsexpval 40035 mhphf 40044 hbtlem4 40702 idomrootle 40771 isdomn3 40780 mon1psubm 40782 amgm2d 41535 amgm3d 41536 amgm4d 41537 c0rhm 45189 c0rnghm 45190 lidlmsgrp 45203 invginvrid 45422 ply1mulgsumlem4 45449 ply1mulgsum 45450 amgmw2d 46225 |
Copyright terms: Public domain | W3C validator |