![]() |
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 20057 | . 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd)) |
3 | 2 | simprbi 498 | 1 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ‘cfv 6541 CMndccmn 19643 mulGrpcmgp 19982 Ringcrg 20050 CRingccrg 20051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6493 df-fv 6549 df-cring 20053 |
This theorem is referenced by: crngcom 20068 crngbascntr 20072 gsummgp0 20124 prdscrngd 20129 crngbinom 20141 unitabl 20191 subrgcrng 20360 sraassaOLD 21416 mplbas2 21589 evlslem3 21635 evlslem6 21636 evlslem1 21637 evlsgsummul 21647 evls1gsummul 21836 evl1gsummul 21871 mamuvs2 21898 matgsumcl 21954 madetsmelbas 21958 madetsmelbas2 21959 mdetleib2 22082 mdetf 22089 mdetdiaglem 22092 mdetdiag 22093 mdetdiagid 22094 mdetrlin 22096 mdetrsca 22097 mdetralt 22102 mdetuni0 22115 smadiadetlem4 22163 chpscmat 22336 chp0mat 22340 chpidmat 22341 amgmlem 26484 amgm 26485 wilthlem2 26563 wilthlem3 26564 lgseisenlem3 26870 lgseisenlem4 26871 frobrhm 32371 cringm4 32554 mdetpmtr1 32792 pwsgprod 41112 evlsvvvallem 41131 selvvvval 41155 evlselv 41157 mhphf 41167 mgpsumunsn 46991 mgpsumz 46992 mgpsumn 46993 amgmwlem 47803 amgmlemALT 47804 |
Copyright terms: Public domain | W3C validator |