![]() |
Mathbox for Jeff Madsen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rngogrpo | Structured version Visualization version GIF version |
Description: A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ringgrp.1 | ⊢ 𝐺 = (1st ‘𝑅) |
Ref | Expression |
---|---|
rngogrpo | ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringgrp.1 | . . 3 ⊢ 𝐺 = (1st ‘𝑅) | |
2 | 1 | rngoablo 34744 | . 2 ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ AbelOp) |
3 | ablogrpo 28020 | . 2 ⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ∈ wcel 2081 ‘cfv 6230 1st c1st 7548 GrpOpcgr 27962 AbelOpcablo 28017 RingOpscrngo 34730 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3710 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-fv 6238 df-ov 7024 df-1st 7550 df-2nd 7551 df-ablo 28018 df-rngo 34731 |
This theorem is referenced by: rngone0 34747 rngogcl 34748 rngoaass 34750 rngorcan 34753 rngolcan 34754 rngo0cl 34755 rngo0rid 34756 rngo0lid 34757 rngolz 34758 rngorz 34759 rngosn3 34760 rngonegcl 34763 rngoaddneg1 34764 rngoaddneg2 34765 rngosub 34766 rngodm1dm2 34768 rngorn1 34769 rngonegmn1l 34777 rngonegmn1r 34778 rngogrphom 34807 rngohom0 34808 rngohomsub 34809 rngokerinj 34811 keridl 34868 dmncan1 34912 |
Copyright terms: Public domain | W3C validator |