![]() |
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 19230 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | |
2 | ringgrp 18992 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp) |
4 | eqid 2795 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
5 | 4 | subrgss 19226 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
6 | eqid 2795 | . . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | |
7 | 6 | subrgring 19228 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
8 | ringgrp 18992 | . . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp) |
10 | 4 | issubg 18033 | . 2 ⊢ (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝑅 ∈ Grp ∧ 𝐴 ⊆ (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Grp)) |
11 | 3, 5, 9, 10 | syl3anbrc 1336 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 ⊆ wss 3859 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 ↾s cress 16313 Grpcgrp 17861 SubGrpcsubg 18027 Ringcrg 18987 SubRingcsubrg 19221 |
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 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 |
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 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fv 6233 df-ov 7019 df-subg 18030 df-ring 18989 df-subrg 19223 |
This theorem is referenced by: subrg0 19232 subrgbas 19234 subrgacl 19236 issubrg2 19245 subrgint 19247 resrhm 19254 rhmima 19256 subdrgint 19272 primefld0cl 19275 abvres 19300 issubassa2 19813 resspsrmul 19885 subrgpsr 19887 mplbas2 19938 gsumply1subr 20085 zsssubrg 20285 gzrngunitlem 20292 zringlpirlem1 20313 zringcyg 20320 prmirred 20324 zndvds 20378 resubgval 20435 rzgrp 20449 subrgnrg 22965 sranlm 22976 clmsub 23367 clmneg 23368 clmabs 23370 clmsubcl 23373 isncvsngp 23436 cphsqrtcl3 23474 tcphcph 23523 plypf1 24485 dvply2g 24557 taylply2 24639 circgrp 24817 circsubm 24818 jensenlem2 25247 amgmlem 25249 lgseisenlem4 25636 qrng0 25879 qrngneg 25881 subrgchr 30519 nn0archi 30570 drgext0gsca 30598 fedgmullem1 30629 fedgmullem2 30630 rezh 30829 qqhcn 30849 qqhucn 30850 selvval2lem4 38665 fsumcnsrcl 39251 cnsrplycl 39252 rngunsnply 39258 zringsubgval 43929 amgmwlem 44383 |
Copyright terms: Public domain | W3C validator |