# Metamath Proof Explorer

## Theorem subrgid

Description: Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypothesis subrgss.1 ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion subrgid ${⊢}{R}\in \mathrm{Ring}\to {B}\in \mathrm{SubRing}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 subrgss.1 ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 id ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Ring}$
3 1 ressid ${⊢}{R}\in \mathrm{Ring}\to {R}{↾}_{𝑠}{B}={R}$
4 3 2 eqeltrd ${⊢}{R}\in \mathrm{Ring}\to {R}{↾}_{𝑠}{B}\in \mathrm{Ring}$
5 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
6 1 5 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {B}$
7 ssid ${⊢}{B}\subseteq {B}$
8 6 7 jctil ${⊢}{R}\in \mathrm{Ring}\to \left({B}\subseteq {B}\wedge {1}_{{R}}\in {B}\right)$
9 1 5 issubrg ${⊢}{B}\in \mathrm{SubRing}\left({R}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {R}{↾}_{𝑠}{B}\in \mathrm{Ring}\right)\wedge \left({B}\subseteq {B}\wedge {1}_{{R}}\in {B}\right)\right)$
10 2 4 8 9 syl21anbrc ${⊢}{R}\in \mathrm{Ring}\to {B}\in \mathrm{SubRing}\left({R}\right)$