# Metamath Proof Explorer

## Theorem subsubrg

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

Ref Expression
Hypothesis subsubrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
Assertion subsubrg ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({B}\in \mathrm{SubRing}\left({S}\right)↔\left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 subsubrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 subrgrcl ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
3 2 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}\in \mathrm{Ring}$
4 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
5 4 subrgss ${⊢}{B}\in \mathrm{SubRing}\left({S}\right)\to {B}\subseteq {\mathrm{Base}}_{{S}}$
6 5 adantl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {B}\subseteq {\mathrm{Base}}_{{S}}$
7 1 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{{S}}$
8 7 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {A}={\mathrm{Base}}_{{S}}$
9 6 8 sseqtrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {B}\subseteq {A}$
10 1 oveq1i ${⊢}{S}{↾}_{𝑠}{B}=\left({R}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}$
11 ressabs ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\to \left({R}{↾}_{𝑠}{A}\right){↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
12 10 11 syl5eq ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\to {S}{↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
13 9 12 syldan ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {S}{↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
14 eqid ${⊢}{S}{↾}_{𝑠}{B}={S}{↾}_{𝑠}{B}$
15 14 subrgring ${⊢}{B}\in \mathrm{SubRing}\left({S}\right)\to {S}{↾}_{𝑠}{B}\in \mathrm{Ring}$
16 15 adantl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {S}{↾}_{𝑠}{B}\in \mathrm{Ring}$
17 13 16 eqeltrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {R}{↾}_{𝑠}{B}\in \mathrm{Ring}$
18 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
19 18 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
20 19 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
21 9 20 sstrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {B}\subseteq {\mathrm{Base}}_{{R}}$
22 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
23 1 22 subrg1 ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}={1}_{{S}}$
24 23 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {1}_{{R}}={1}_{{S}}$
25 eqid ${⊢}{1}_{{S}}={1}_{{S}}$
26 25 subrg1cl ${⊢}{B}\in \mathrm{SubRing}\left({S}\right)\to {1}_{{S}}\in {B}$
27 26 adantl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {1}_{{S}}\in {B}$
28 24 27 eqeltrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {1}_{{R}}\in {B}$
29 21 28 jca ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({B}\subseteq {\mathrm{Base}}_{{R}}\wedge {1}_{{R}}\in {B}\right)$
30 18 22 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 {\mathrm{Base}}_{{R}}\wedge {1}_{{R}}\in {B}\right)\right)$
31 3 17 29 30 syl21anbrc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to {B}\in \mathrm{SubRing}\left({R}\right)$
32 31 9 jca ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)$
33 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
34 33 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {S}\in \mathrm{Ring}$
35 12 adantrl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {S}{↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
36 eqid ${⊢}{R}{↾}_{𝑠}{B}={R}{↾}_{𝑠}{B}$
37 36 subrgring ${⊢}{B}\in \mathrm{SubRing}\left({R}\right)\to {R}{↾}_{𝑠}{B}\in \mathrm{Ring}$
38 37 ad2antrl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {R}{↾}_{𝑠}{B}\in \mathrm{Ring}$
39 35 38 eqeltrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {S}{↾}_{𝑠}{B}\in \mathrm{Ring}$
40 simprr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {B}\subseteq {A}$
41 7 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {A}={\mathrm{Base}}_{{S}}$
42 40 41 sseqtrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {B}\subseteq {\mathrm{Base}}_{{S}}$
43 23 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {1}_{{R}}={1}_{{S}}$
44 22 subrg1cl ${⊢}{B}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}\in {B}$
45 44 ad2antrl ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {1}_{{R}}\in {B}$
46 43 45 eqeltrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {1}_{{S}}\in {B}$
47 42 46 jca ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to \left({B}\subseteq {\mathrm{Base}}_{{S}}\wedge {1}_{{S}}\in {B}\right)$
48 4 25 issubrg ${⊢}{B}\in \mathrm{SubRing}\left({S}\right)↔\left(\left({S}\in \mathrm{Ring}\wedge {S}{↾}_{𝑠}{B}\in \mathrm{Ring}\right)\wedge \left({B}\subseteq {\mathrm{Base}}_{{S}}\wedge {1}_{{S}}\in {B}\right)\right)$
49 34 39 47 48 syl21anbrc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge \left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)\to {B}\in \mathrm{SubRing}\left({S}\right)$
50 32 49 impbida ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({B}\in \mathrm{SubRing}\left({S}\right)↔\left({B}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\subseteq {A}\right)\right)$