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 ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ R ∧ B ⊆ A

Proof

Step Hyp Ref Expression
1 subsubrg.s ⊢ S = R ↾ 𝑠 A
2 subrgrcl ⊢ A ∈ SubRing ⁡ R → R ∈ Ring
3 2 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → R ∈ Ring
4 eqid ⊢ Base S = Base S
5 4 subrgss ⊢ B ∈ SubRing ⁡ S → B ⊆ Base S
6 5 adantl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ⊆ Base S
7 1 subrgbas ⊢ A ∈ SubRing ⁡ R → A = Base S
8 7 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → A = Base S
9 6 8 sseqtrrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ⊆ A
10 1 oveq1i ⊢ S ↾ 𝑠 B = R ↾ 𝑠 A ↾ 𝑠 B
11 ressabs ⊢ A ∈ SubRing ⁡ R ∧ B ⊆ A → R ↾ 𝑠 A ↾ 𝑠 B = R ↾ 𝑠 B
12 10 11 syl5eq ⊢ A ∈ SubRing ⁡ R ∧ B ⊆ A → S ↾ 𝑠 B = R ↾ 𝑠 B
13 9 12 syldan ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → S ↾ 𝑠 B = R ↾ 𝑠 B
14 eqid ⊢ S ↾ 𝑠 B = S ↾ 𝑠 B
15 14 subrgring ⊢ B ∈ SubRing ⁡ S → S ↾ 𝑠 B ∈ Ring
16 15 adantl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → S ↾ 𝑠 B ∈ Ring
17 13 16 eqeltrrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → R ↾ 𝑠 B ∈ Ring
18 eqid ⊢ Base R = Base R
19 18 subrgss ⊢ A ∈ SubRing ⁡ R → A ⊆ Base R
20 19 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → A ⊆ Base R
21 9 20 sstrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ⊆ Base R
22 eqid ⊢ 1 R = 1 R
23 1 22 subrg1 ⊢ A ∈ SubRing ⁡ R → 1 R = 1 S
24 23 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → 1 R = 1 S
25 eqid ⊢ 1 S = 1 S
26 25 subrg1cl ⊢ B ∈ SubRing ⁡ S → 1 S ∈ B
27 26 adantl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → 1 S ∈ B
28 24 27 eqeltrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → 1 R ∈ B
29 21 28 jca ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ⊆ Base R ∧ 1 R ∈ B
30 18 22 issubrg ⊢ B ∈ SubRing ⁡ R ↔ R ∈ Ring ∧ R ↾ 𝑠 B ∈ Ring ∧ B ⊆ Base R ∧ 1 R ∈ B
31 3 17 29 30 syl21anbrc ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ∈ SubRing ⁡ R
32 31 9 jca ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ S → B ∈ SubRing ⁡ R ∧ B ⊆ A
33 1 subrgring ⊢ A ∈ SubRing ⁡ R → S ∈ Ring
34 33 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → S ∈ Ring
35 12 adantrl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → S ↾ 𝑠 B = R ↾ 𝑠 B
36 eqid ⊢ R ↾ 𝑠 B = R ↾ 𝑠 B
37 36 subrgring ⊢ B ∈ SubRing ⁡ R → R ↾ 𝑠 B ∈ Ring
38 37 ad2antrl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → R ↾ 𝑠 B ∈ Ring
39 35 38 eqeltrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → S ↾ 𝑠 B ∈ Ring
40 simprr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → B ⊆ A
41 7 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → A = Base S
42 40 41 sseqtrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → B ⊆ Base S
43 23 adantr ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → 1 R = 1 S
44 22 subrg1cl ⊢ B ∈ SubRing ⁡ R → 1 R ∈ B
45 44 ad2antrl ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → 1 R ∈ B
46 43 45 eqeltrrd ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → 1 S ∈ B
47 42 46 jca ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → B ⊆ Base S ∧ 1 S ∈ B
48 4 25 issubrg ⊢ B ∈ SubRing ⁡ S ↔ S ∈ Ring ∧ S ↾ 𝑠 B ∈ Ring ∧ B ⊆ Base S ∧ 1 S ∈ B
49 34 39 47 48 syl21anbrc ⊢ A ∈ SubRing ⁡ R ∧ B ∈ SubRing ⁡ R ∧ B ⊆ A → B ∈ SubRing ⁡ S
50 32 49 impbida ⊢ A ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ R ∧ B ⊆ A