subsubrng

Description: A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025)

		Ref	Expression
	Hypothesis	subsubrng.s	$⊢ S = R ↾_{𝑠} A$
	Assertion	subsubrng	$⊢ A \in SubRng (R) \to (B \in SubRng (S) \leftrightarrow (B \in SubRng (R) \land B \subseteq A))$

Proof

Step	Hyp	Ref	Expression
1		subsubrng.s	$⊢ S = R ↾_{𝑠} A$
2		subrngrcl	$⊢ A \in SubRng (R) \to R \in Rng$
3	2	adantr	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to R \in Rng$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5	4	subrngss	$⊢ B \in SubRng (S) \to B \subseteq {Base}_{S}$
6	5	adantl	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to B \subseteq {Base}_{S}$
7	1	subrngbas	$⊢ A \in SubRng (R) \to A = {Base}_{S}$
8	7	adantr	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to A = {Base}_{S}$
9	6 8	sseqtrrd	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to B \subseteq A$
10	1	oveq1i	$⊢ S ↾_{𝑠} B = (R ↾_{𝑠} A) ↾_{𝑠} B$
11		ressabs	$⊢ (A \in SubRng (R) \land B \subseteq A) \to (R ↾_{𝑠} A) ↾_{𝑠} B = R ↾_{𝑠} B$
12	10 11	eqtrid	$⊢ (A \in SubRng (R) \land B \subseteq A) \to S ↾_{𝑠} B = R ↾_{𝑠} B$
13	9 12	syldan	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to S ↾_{𝑠} B = R ↾_{𝑠} B$
14		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
15	14	subrngrng	$⊢ B \in SubRng (S) \to S ↾_{𝑠} B \in Rng$
16	15	adantl	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to S ↾_{𝑠} B \in Rng$
17	13 16	eqeltrrd	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to R ↾_{𝑠} B \in Rng$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19	18	subrngss	$⊢ A \in SubRng (R) \to A \subseteq {Base}_{R}$
20	19	adantr	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to A \subseteq {Base}_{R}$
21	9 20	sstrd	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to B \subseteq {Base}_{R}$
22	18	issubrng	$⊢ B \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} B \in Rng \land B \subseteq {Base}_{R})$
23	3 17 21 22	syl3anbrc	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to B \in SubRng (R)$
24	23 9	jca	$⊢ (A \in SubRng (R) \land B \in SubRng (S)) \to (B \in SubRng (R) \land B \subseteq A)$
25	1	subrngrng	$⊢ A \in SubRng (R) \to S \in Rng$
26	25	adantr	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to S \in Rng$
27	12	adantrl	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to S ↾_{𝑠} B = R ↾_{𝑠} B$
28		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
29	28	subrngrng	$⊢ B \in SubRng (R) \to R ↾_{𝑠} B \in Rng$
30	29	ad2antrl	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to R ↾_{𝑠} B \in Rng$
31	27 30	eqeltrd	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to S ↾_{𝑠} B \in Rng$
32		simprr	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to B \subseteq A$
33	7	adantr	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to A = {Base}_{S}$
34	32 33	sseqtrd	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to B \subseteq {Base}_{S}$
35	4	issubrng	$⊢ B \in SubRng (S) \leftrightarrow (S \in Rng \land S ↾_{𝑠} B \in Rng \land B \subseteq {Base}_{S})$
36	26 31 34 35	syl3anbrc	$⊢ (A \in SubRng (R) \land (B \in SubRng (R) \land B \subseteq A)) \to B \in SubRng (S)$
37	24 36	impbida	$⊢ A \in SubRng (R) \to (B \in SubRng (S) \leftrightarrow (B \in SubRng (R) \land B \subseteq A))$

Metamath Proof Explorer

Theorem subsubrng

Proof