subrgmpl

Description: A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	subrgmpl.s	$⊢ S = I mPoly R$
	subrgmpl.h	$⊢ H = R ↾_{𝑠} T$
	subrgmpl.u	$⊢ U = I mPoly H$
	subrgmpl.b	$⊢ B = {Base}_{U}$
Assertion	subrgmpl	$⊢ (I \in V \land T \in SubRing (R)) \to B \in SubRing (S)$

Proof

Step	Hyp	Ref	Expression
1		subrgmpl.s	$⊢ S = I mPoly R$
2		subrgmpl.h	$⊢ H = R ↾_{𝑠} T$
3		subrgmpl.u	$⊢ U = I mPoly H$
4		subrgmpl.b	$⊢ B = {Base}_{U}$
5		simpl	$⊢ (I \in V \land T \in SubRing (R)) \to I \in V$
6		simpr	$⊢ (I \in V \land T \in SubRing (R)) \to T \in SubRing (R)$
7		eqid	$⊢ I mPwSer H = I mPwSer H$
8		eqid	$⊢ {Base}_{(I mPwSer H)} = {Base}_{(I mPwSer H)}$
9		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10	1 2 3 4 5 6 7 8 9	ressmplbas2	$⊢ (I \in V \land T \in SubRing (R)) \to B = {Base}_{(I mPwSer H)} \cap {Base}_{S}$
11		eqid	$⊢ I mPwSer R = I mPwSer R$
12	11 2 7 8	subrgpsr	$⊢ (I \in V \land T \in SubRing (R)) \to {Base}_{(I mPwSer H)} \in SubRing (I mPwSer R)$
13		subrgrcl	$⊢ T \in SubRing (R) \to R \in Ring$
14	13	adantl	$⊢ (I \in V \land T \in SubRing (R)) \to R \in Ring$
15	11 1 9 5 14	mplsubrg	$⊢ (I \in V \land T \in SubRing (R)) \to {Base}_{S} \in SubRing (I mPwSer R)$
16		subrgin	$⊢ ({Base}_{(I mPwSer H)} \in SubRing (I mPwSer R) \land {Base}_{S} \in SubRing (I mPwSer R)) \to {Base}_{(I mPwSer H)} \cap {Base}_{S} \in SubRing (I mPwSer R)$
17	12 15 16	syl2anc	$⊢ (I \in V \land T \in SubRing (R)) \to {Base}_{(I mPwSer H)} \cap {Base}_{S} \in SubRing (I mPwSer R)$
18	10 17	eqeltrd	$⊢ (I \in V \land T \in SubRing (R)) \to B \in SubRing (I mPwSer R)$
19		inss2	$⊢ {Base}_{(I mPwSer H)} \cap {Base}_{S} \subseteq {Base}_{S}$
20	10 19	eqsstrdi	$⊢ (I \in V \land T \in SubRing (R)) \to B \subseteq {Base}_{S}$
21	1 11 9	mplval2	$⊢ S = (I mPwSer R) ↾_{𝑠} {Base}_{S}$
22	21	subsubrg	$⊢ {Base}_{S} \in SubRing (I mPwSer R) \to (B \in SubRing (S) \leftrightarrow (B \in SubRing (I mPwSer R) \land B \subseteq {Base}_{S}))$
23	15 22	syl	$⊢ (I \in V \land T \in SubRing (R)) \to (B \in SubRing (S) \leftrightarrow (B \in SubRing (I mPwSer R) \land B \subseteq {Base}_{S}))$
24	18 20 23	mpbir2and	$⊢ (I \in V \land T \in SubRing (R)) \to B \in SubRing (S)$

Metamath Proof Explorer

Theorem subrgmpl

Proof