| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ringgrp | GIF version | ||
| Description: A ring is a group. (Contributed by NM, 15-Sep-2011.) |
| Ref | Expression |
|---|---|
| ringgrp | ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2206 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 2 | eqid 2206 | . . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅) | |
| 3 | eqid 2206 | . . 3 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
| 4 | eqid 2206 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
| 5 | 1, 2, 3, 4 | isring 13812 | . 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))))) |
| 6 | 5 | simp1bi 1015 | 1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 ∈ wcel 2177 ∀wral 2485 ‘cfv 5277 (class class class)co 5954 Basecbs 12882 +gcplusg 12959 .rcmulr 12960 Mndcmnd 13298 Grpcgrp 13382 mulGrpcmgp 13732 Ringcrg 13808 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4167 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-cnex 8029 ax-resscn 8030 ax-1re 8032 ax-addrcl 8035 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3001 df-un 3172 df-in 3174 df-ss 3181 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-int 3889 df-br 4049 df-opab 4111 df-mpt 4112 df-id 4345 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-iota 5238 df-fun 5279 df-fn 5280 df-fv 5285 df-ov 5957 df-inn 9050 df-2 9108 df-3 9109 df-ndx 12885 df-slot 12886 df-base 12888 df-plusg 12972 df-mulr 12973 df-ring 13810 |
| This theorem is referenced by: ringgrpd 13817 ringmnd 13818 ring0cl 13833 ringacl 13842 ringcom 13843 ringabl 13844 ringlz 13855 ringrz 13856 ringnegl 13863 ringnegr 13864 ringmneg1 13865 ringmneg2 13866 ringm2neg 13867 ringsubdi 13868 ringsubdir 13869 mulgass2 13870 ringlghm 13873 ringrghm 13874 ringressid 13875 imasring 13876 opprring 13891 dvdsrneg 13915 unitnegcl 13942 dvrdir 13955 dfrhm2 13966 isrhm 13970 isrhmd 13978 rhmfn 13984 rhmval 13985 subrgsubg 14039 lmodfgrp 14108 lmod0vs 14133 lmodvsneg 14143 lmodsubvs 14155 lmodsubdi 14156 lmodsubdir 14157 rmodislmodlem 14162 rmodislmod 14163 issubrgd 14264 lidlsubg 14298 cnfld0 14383 cnfldneg 14385 cnfldsub 14387 cnsubglem 14391 zringgrp 14407 mulgrhm 14421 zrhmulg 14432 |
| Copyright terms: Public domain | W3C validator |