Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > crngmgp | Structured version Visualization version GIF version |
Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Ref | Expression |
---|---|
ringmgp.g | ⊢ 𝐺 = (mulGrp‘𝑅) |
Ref | Expression |
---|---|
crngmgp | ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringmgp.g | . . 3 ⊢ 𝐺 = (mulGrp‘𝑅) | |
2 | 1 | iscrng 19523 | . 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd)) |
3 | 2 | simprbi 500 | 1 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 ‘cfv 6358 CMndccmn 19124 mulGrpcmgp 19458 Ringcrg 19516 CRingccrg 19517 |
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 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
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-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-cring 19519 |
This theorem is referenced by: crngcom 19534 gsummgp0 19580 prdscrngd 19585 crngbinom 19593 unitabl 19640 subrgcrng 19758 sraassa 20783 mplbas2 20953 evlslem3 20994 evlslem6 20995 evlslem1 20996 evlsgsummul 21006 evls1gsummul 21195 evl1gsummul 21230 mamuvs2 21257 matgsumcl 21311 madetsmelbas 21315 madetsmelbas2 21316 mdetleib2 21439 mdetf 21446 mdetdiaglem 21449 mdetdiag 21450 mdetdiagid 21451 mdetrlin 21453 mdetrsca 21454 mdetralt 21459 mdetuni0 21472 smadiadetlem4 21520 chpscmat 21693 chp0mat 21697 chpidmat 21698 amgmlem 25826 amgm 25827 wilthlem2 25905 wilthlem3 25906 lgseisenlem3 26212 lgseisenlem4 26213 frobrhm 31158 cringm4 31290 mdetpmtr1 31441 pwsgprod 39922 evlsbagval 39926 mhphf 39936 mgpsumunsn 45313 mgpsumz 45314 mgpsumn 45315 amgmwlem 46120 amgmlemALT 46121 |
Copyright terms: Public domain | W3C validator |