# Metamath Proof Explorer

## Theorem subrgsubg

Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Assertion subrgsubg ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\in \mathrm{SubGrp}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 subrgrcl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
2 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
3 1 2 syl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Grp}$
4 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
5 4 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
6 eqid ${⊢}{R}{↾}_{𝑠}{A}={R}{↾}_{𝑠}{A}$
7 6 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}{↾}_{𝑠}{A}\in \mathrm{Ring}$
8 ringgrp ${⊢}{R}{↾}_{𝑠}{A}\in \mathrm{Ring}\to {R}{↾}_{𝑠}{A}\in \mathrm{Grp}$
9 7 8 syl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}{↾}_{𝑠}{A}\in \mathrm{Grp}$
10 4 issubg ${⊢}{A}\in \mathrm{SubGrp}\left({R}\right)↔\left({R}\in \mathrm{Grp}\wedge {A}\subseteq {\mathrm{Base}}_{{R}}\wedge {R}{↾}_{𝑠}{A}\in \mathrm{Grp}\right)$
11 3 5 9 10 syl3anbrc ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\in \mathrm{SubGrp}\left({R}\right)$