# Metamath Proof Explorer

## Theorem issubrg2

Description: Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubrg2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
issubrg2.o
issubrg2.t
Assertion issubrg2

### Proof

Step Hyp Ref Expression
1 issubrg2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 issubrg2.o
3 issubrg2.t
4 subrgsubg ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\in \mathrm{SubGrp}\left({R}\right)$
5 2 subrg1cl
6 3 subrgmcl
7 6 3expb
8 7 ralrimivva
9 4 5 8 3jca
10 simpl
11 simpr1
12 eqid ${⊢}{R}{↾}_{𝑠}{A}={R}{↾}_{𝑠}{A}$
13 12 subgbas ${⊢}{A}\in \mathrm{SubGrp}\left({R}\right)\to {A}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
14 11 13 syl
15 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
16 12 15 ressplusg ${⊢}{A}\in \mathrm{SubGrp}\left({R}\right)\to {+}_{{R}}={+}_{\left({R}{↾}_{𝑠}{A}\right)}$
17 11 16 syl
18 12 3 ressmulr
19 11 18 syl
20 12 subggrp ${⊢}{A}\in \mathrm{SubGrp}\left({R}\right)\to {R}{↾}_{𝑠}{A}\in \mathrm{Grp}$
21 11 20 syl
22 simpr3
23 oveq1
24 23 eleq1d
25 oveq2
26 25 eleq1d
27 24 26 rspc2v
28 22 27 syl5com
29 28 3impib
30 1 subgss ${⊢}{A}\in \mathrm{SubGrp}\left({R}\right)\to {A}\subseteq {B}$
31 11 30 syl
32 31 sseld
33 31 sseld
34 31 sseld
35 32 33 34 3anim123d
36 35 imp
37 1 3 ringass
39 36 38 syldan
40 1 15 3 ringdi
42 36 41 syldan
43 1 15 3 ringdir
45 36 44 syldan
46 simpr2
47 32 imp
48 1 3 2 ringlidm