![]() |
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 19100 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | |
2 | ringgrp 18865 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp) |
4 | eqid 2798 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
5 | 4 | subrgss 19096 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
6 | eqid 2798 | . . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | |
7 | 6 | subrgring 19098 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
8 | ringgrp 18865 | . . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp) |
10 | 4 | issubg 17904 | . 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp)) |
11 | 3, 5, 9, 10 | syl3anbrc 1444 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 ⊆ wss 3768 ‘cfv 6100 (class class class)co 6877 Basecbs 16181 ↾s cress 16182 Grpcgrp 17735 SubGrpcsubg 17898 Ringcrg 18860 SubRingcsubrg 19091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 ax-sep 4974 ax-nul 4982 ax-pow 5034 ax-pr 5096 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3386 df-sbc 3633 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-pw 4350 df-sn 4368 df-pr 4370 df-op 4374 df-uni 4628 df-br 4843 df-opab 4905 df-mpt 4922 df-id 5219 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-iota 6063 df-fun 6102 df-fv 6108 df-ov 6880 df-subg 17901 df-ring 18862 df-subrg 19093 |
This theorem is referenced by: subrg0 19102 subrgbas 19104 subrgacl 19106 issubrg2 19115 subrgint 19117 resrhm 19124 rhmima 19126 abvres 19154 issubassa2 19665 resspsrmul 19737 subrgpsr 19739 mplbas2 19790 gsumply1subr 19923 zsssubrg 20123 gzrngunitlem 20130 zringlpirlem1 20151 zringcyg 20158 prmirred 20162 zndvds 20216 resubgval 20275 rzgrp 20289 subrgnrg 22802 sranlm 22813 clmsub 23204 clmneg 23205 clmabs 23207 clmsubcl 23210 isncvsngp 23273 cphsqrtcl3 23311 tcphcph 23360 plypf1 24306 dvply2g 24378 taylply2 24460 circgrp 24637 circsubm 24638 jensenlem2 25063 amgmlem 25065 lgseisenlem4 25452 qrng0 25659 qrngneg 25661 subrgchr 30303 nn0archi 30352 rezh 30524 qqhcn 30544 qqhucn 30545 fsumcnsrcl 38510 cnsrplycl 38511 rngunsnply 38517 zringsubgval 42971 amgmwlem 43339 |
Copyright terms: Public domain | W3C validator |