| 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 20555 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | |
| 2 | ringgrp 20217 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp) |
| 4 | eqid 2740 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 5 | 4 | subrgss 20551 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
| 6 | eqid 2740 | . . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | |
| 7 | 6 | subrgring 20553 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
| 8 | ringgrp 20217 | . . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | |
| 9 | 7, 8 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp) |
| 10 | 4 | issubg 19100 | . 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp)) |
| 11 | 3, 5, 9, 10 | syl3anbrc 1350 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2119 ⊆ wss 3890 ‘cfv 6492 (class class class)co 7363 Basecbs 17177 ↾s cress 17198 Grpcgrp 18907 SubGrpcsubg 19094 Ringcrg 20212 SubRingcsubrg 20548 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-sbc 3731 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7366 df-subg 19097 df-ring 20214 df-subrg 20549 |
| This theorem is referenced by: subrg0 20558 subrgbas 20560 subrgacl 20562 issubrg2 20571 subrgint 20574 resrhm 20580 resrhm2b 20581 rhmima 20583 subdrgint 20782 primefld0cl 20785 abvres 20810 zsssubrg 21407 gzrngunitlem 21414 zringlpirlem1 21444 zringcyg 21451 zringsubgval 21452 prmirred 21456 zndvds 21531 resubgval 21591 rzgrp 21605 issubassa2 21874 resspsrmul 21957 subrgpsr 21959 mplbas2 22025 gsumply1subr 22225 subrgnrg 24663 sranlm 24674 clmsub 25072 clmneg 25073 clmabs 25075 clmsubcl 25078 isncvsngp 25141 cphsqrtcl3 25179 tcphcph 25229 plypf1 26202 dvply2g 26276 taylply2 26358 circgrp 26541 circsubm 26542 jensenlem2 26976 amgmlem 26978 lgseisenlem4 27366 qrng0 27609 qrngneg 27611 subrgchr 33325 elrgspnlem4 33333 elrgspnsubrunlem2 33336 subrdom 33373 1fldgenq 33413 nn0archi 33437 idlinsubrg 33521 ressply1evls1 33655 ressply10g 33657 ressply1invg 33659 ressply1sub 33660 evls1subd 33662 vr1nz 33683 drgext0gsca 33783 fedgmullem1 33820 fedgmullem2 33821 evls1fldgencl 33861 fldextrspunlsplem 33864 fldextrspunlsp 33865 irngss 33878 extdgfialglem1 33883 extdgfialglem2 33884 algextdeglem1 33908 algextdeglem2 33909 algextdeglem3 33910 algextdeglem4 33911 algextdeglem5 33912 rtelextdg2lem 33917 constrelextdg2 33938 2sqr3minply 33971 rezh 34160 qqhcn 34182 qqhucn 34183 fsumcnsrcl 43618 cnsrplycl 43619 rngunsnply 43621 amgmwlem 50299 |
| Copyright terms: Public domain | W3C validator |