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 SubRing (R) \to (B \in SubRing (S) \leftrightarrow (B \in SubRing (R) \land B \subseteq A))$

Proof

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

Metamath Proof Explorer

Theorem subsubrg

Proof