Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ringmgp | Structured version Visualization version Unicode version |
Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
Ref | Expression |
---|---|
ringmgp.g | mulGrp |
Ref | Expression |
---|---|
ringmgp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2622 | . . 3 | |
2 | ringmgp.g | . . 3 mulGrp | |
3 | eqid 2622 | . . 3 | |
4 | eqid 2622 | . . 3 | |
5 | 1, 2, 3, 4 | isring 18551 | . 2 |
6 | 5 | simp2bi 1077 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wcel 1990 wral 2912 cfv 5888 (class class class)co 6650 cbs 15857 cplusg 15941 cmulr 15942 cmnd 17294 cgrp 17422 mulGrpcmgp 18489 crg 18547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-ring 18549 |
This theorem is referenced by: mgpf 18559 ringcl 18561 iscrng2 18563 ringass 18564 ringideu 18565 ringidcl 18568 ringidmlem 18570 ringsrg 18589 unitsubm 18670 dfrhm2 18717 isrhm2d 18728 idrhm 18731 pwsco1rhm 18738 pwsco2rhm 18739 subrgcrng 18784 subrgsubm 18793 issubrg3 18808 cntzsubr 18812 pwsdiagrhm 18813 assamulgscmlem2 19349 psrcrng 19413 mplcoe3 19466 mplcoe5lem 19467 mplcoe5 19468 ply1moncl 19641 coe1pwmul 19649 ply1coefsupp 19665 ply1coe 19666 gsummoncoe1 19674 lply1binomsc 19677 evls1gsummul 19690 evl1expd 19709 evl1gsummul 19724 evl1scvarpw 19727 evl1scvarpwval 19728 evl1gsummon 19729 cnfldexp 19779 expmhm 19815 nn0srg 19816 rge0srg 19817 ringvcl 20204 mat1mhm 20290 scmatmhm 20340 m1detdiag 20403 mdetdiaglem 20404 m2detleiblem2 20434 mat2pmatmhm 20538 pmatcollpwscmatlem1 20594 mply1topmatcllem 20608 mply1topmatcl 20610 pm2mpghm 20621 pm2mpmhm 20625 monmat2matmon 20629 pm2mp 20630 chpscmatgsumbin 20649 chpscmatgsummon 20650 chfacfscmulcl 20662 chfacfscmul0 20663 chfacfpmmulcl 20666 chfacfpmmul0 20667 chfacfpmmulgsum2 20670 cayhamlem1 20671 cpmadugsumlemB 20679 cpmadugsumlemC 20680 cpmadugsumlemF 20681 cayhamlem2 20689 cayhamlem4 20693 nrgtrg 22494 deg1pw 23880 plypf1 23968 efsubm 24297 amgm 24717 wilthlem2 24795 wilthlem3 24796 dchrelbas3 24963 lgsqrlem2 25072 lgsqrlem3 25073 lgsqrlem4 25074 psgnid 29847 iistmd 29948 hbtlem4 37696 subrgacs 37770 idomrootle 37773 isdomn3 37782 mon1psubm 37784 amgm2d 38501 amgm3d 38502 amgm4d 38503 c0rhm 41912 c0rnghm 41913 lidlmsgrp 41926 invginvrid 42148 ply1mulgsumlem4 42177 ply1mulgsum 42178 amgmw2d 42550 |
Copyright terms: Public domain | W3C validator |