| 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 20548 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) | |
| 2 | ringgrp 20210 | . . 3 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Grp) |
| 4 | eqid 2739 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 5 | 4 | subrgss 20544 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
| 6 | eqid 2739 | . . . 4 ⊢ (𝑅 ↾s 𝐴) = (𝑅 ↾s 𝐴) | |
| 7 | 6 | subrgring 20546 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Ring) |
| 8 | ringgrp 20210 | . . 3 ⊢ ((𝑅 ↾s 𝐴) ∈ Ring → (𝑅 ↾s 𝐴) ∈ Grp) | |
| 9 | 7, 8 | syl 17 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐴) ∈ Grp) |
| 10 | 4 | issubg 19093 | . 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 3883 ‘cfv 6485 (class class class)co 7356 Basecbs 17170 ↾s cress 17191 Grpcgrp 18900 SubGrpcsubg 19087 Ringcrg 20205 SubRingcsubrg 20541 |
| 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 2711 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 |
| 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 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-sbc 3724 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fv 6493 df-ov 7359 df-subg 19090 df-ring 20207 df-subrg 20542 |
| This theorem is referenced by: subrg0 20551 subrgbas 20553 subrgacl 20555 issubrg2 20564 subrgint 20567 resrhm 20573 resrhm2b 20574 rhmima 20576 subdrgint 20775 primefld0cl 20778 abvres 20803 zsssubrg 21400 gzrngunitlem 21407 zringlpirlem1 21437 zringcyg 21444 zringsubgval 21445 prmirred 21449 zndvds 21524 resubgval 21584 rzgrp 21598 issubassa2 21867 resspsrmul 21950 subrgpsr 21952 mplbas2 22018 gsumply1subr 22218 subrgnrg 24656 sranlm 24667 clmsub 25065 clmneg 25066 clmabs 25068 clmsubcl 25071 isncvsngp 25134 cphsqrtcl3 25172 tcphcph 25222 plypf1 26195 dvply2g 26269 taylply2 26351 circgrp 26534 circsubm 26535 jensenlem2 26969 amgmlem 26971 lgseisenlem4 27359 qrng0 27602 qrngneg 27604 subrgchr 33318 elrgspnlem4 33326 elrgspnsubrunlem2 33329 subrdom 33366 1fldgenq 33406 nn0archi 33430 idlinsubrg 33514 ressply1evls1 33648 ressply10g 33650 ressply1invg 33652 ressply1sub 33653 evls1subd 33655 vr1nz 33676 drgext0gsca 33776 fedgmullem1 33813 fedgmullem2 33814 evls1fldgencl 33854 fldextrspunlsplem 33857 fldextrspunlsp 33858 irngss 33871 extdgfialglem1 33876 extdgfialglem2 33877 algextdeglem1 33901 algextdeglem2 33902 algextdeglem3 33903 algextdeglem4 33904 algextdeglem5 33905 rtelextdg2lem 33910 constrelextdg2 33931 2sqr3minply 33964 rezh 34153 qqhcn 34175 qqhucn 34176 fsumcnsrcl 43611 cnsrplycl 43612 rngunsnply 43614 amgmwlem 50292 |
| Copyright terms: Public domain | W3C validator |