| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > subrgsubg | Structured version Visualization version GIF version | ||
| Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.) |
| Ref | Expression |
|---|---|
| subrgsubg | ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subrgrcl 20576 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | |
| 2 | ringgrp 20235 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp) |
| 4 | eqid 2737 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 5 | 4 | subrgss 20572 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
| 6 | eqid 2737 | . . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | |
| 7 | 6 | subrgring 20574 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
| 8 | ringgrp 20235 | . . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | |
| 9 | 7, 8 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp) |
| 10 | 4 | issubg 19144 | . 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp)) |
| 11 | 3, 5, 9, 10 | syl3anbrc 1344 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ⊆ wss 3951 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 ↾s cress 17274 Grpcgrp 18951 SubGrpcsubg 19138 Ringcrg 20230 SubRingcsubrg 20569 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fv 6569 df-ov 7434 df-subg 19141 df-ring 20232 df-subrg 20570 |
| This theorem is referenced by: subrg0 20579 subrgbas 20581 subrgacl 20583 issubrg2 20592 subrgint 20595 resrhm 20601 resrhm2b 20602 rhmima 20604 subdrgint 20804 primefld0cl 20807 abvres 20832 zsssubrg 21443 gzrngunitlem 21450 zringlpirlem1 21473 zringcyg 21480 zringsubgval 21481 prmirred 21485 zndvds 21568 resubgval 21627 rzgrp 21641 issubassa2 21912 resspsrmul 21996 subrgpsr 21998 mplbas2 22060 gsumply1subr 22235 subrgnrg 24694 sranlm 24705 clmsub 25113 clmneg 25114 clmabs 25116 clmsubcl 25119 isncvsngp 25183 cphsqrtcl3 25221 tcphcph 25271 plypf1 26251 dvply2g 26326 dvply2gOLD 26327 taylply2 26409 taylply2OLD 26410 circgrp 26594 circsubm 26595 jensenlem2 27031 amgmlem 27033 lgseisenlem4 27422 qrng0 27665 qrngneg 27667 subrgchr 33241 elrgspnlem4 33249 elrgspnsubrunlem2 33252 subrdom 33288 1fldgenq 33324 nn0archi 33375 idlinsubrg 33459 ressply10g 33592 ressply1invg 33594 ressply1sub 33595 evls1subd 33597 drgext0gsca 33642 fedgmullem1 33680 fedgmullem2 33681 evls1fldgencl 33720 fldextrspunlsplem 33723 fldextrspunlsp 33724 irngss 33737 algextdeglem1 33758 algextdeglem2 33759 algextdeglem3 33760 algextdeglem4 33761 algextdeglem5 33762 rtelextdg2lem 33767 constrelextdg2 33788 2sqr3minply 33791 rezh 33970 qqhcn 33992 qqhucn 33993 fsumcnsrcl 43178 cnsrplycl 43179 rngunsnply 43181 amgmwlem 49321 |
| Copyright terms: Public domain | W3C validator |