mpfsubrg

Description: Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 6-May-2015) (Revised by AV, 19-Sep-2021)

		Ref	Expression
	Hypothesis	mpfsubrg.q	$⊢ Q = ran (I evalSub S) (R)$
	Assertion	mpfsubrg	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	$⊢ Q = ran (I evalSub S) (R)$
2		eqid	$⊢ (I evalSub S) (R) = (I evalSub S) (R)$
3		eqid	$⊢ I mPoly (S ↾_{𝑠} R) = I mPoly (S ↾_{𝑠} R)$
4		eqid	$⊢ S ↾_{𝑠} R = S ↾_{𝑠} R$
5		eqid	$⊢ S ↑_{𝑠} ({Base}_{S}^{I}) = S ↑_{𝑠} ({Base}_{S}^{I})$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7	2 3 4 5 6	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} ({Base}_{S}^{I})))$
8		eqid	$⊢ {Base}_{(I mPoly (S ↾_{𝑠} R))} = {Base}_{(I mPoly (S ↾_{𝑠} R))}$
9		eqid	$⊢ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))} = {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
10	8 9	rhmf	$⊢ (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} ({Base}_{S}^{I}))) \to (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
11		ffn	$⊢ (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))} \to (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))}$
12		fnima	$⊢ (I evalSub S) (R) Fn {Base}_{(I mPoly (S ↾_{𝑠} R))} \to (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}] = ran (I evalSub S) (R)$
13	11 12	syl	$⊢ (I evalSub S) (R) : {Base}_{(I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))} \to (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}] = ran (I evalSub S) (R)$
14	7 10 13	3syl	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}] = ran (I evalSub S) (R)$
15	1 14	eqtr4id	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q = (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}]$
16	4	subrgring	$⊢ R \in SubRing (S) \to S ↾_{𝑠} R \in Ring$
17	3	mplring	$⊢ (I \in V \land S ↾_{𝑠} R \in Ring) \to I mPoly (S ↾_{𝑠} R) \in Ring$
18	16 17	sylan2	$⊢ (I \in V \land R \in SubRing (S)) \to I mPoly (S ↾_{𝑠} R) \in Ring$
19	18	3adant2	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to I mPoly (S ↾_{𝑠} R) \in Ring$
20	8	subrgid	$⊢ I mPoly (S ↾_{𝑠} R) \in Ring \to {Base}_{(I mPoly (S ↾_{𝑠} R))} \in SubRing (I mPoly (S ↾_{𝑠} R))$
21	19 20	syl	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to {Base}_{(I mPoly (S ↾_{𝑠} R))} \in SubRing (I mPoly (S ↾_{𝑠} R))$
22		rhmima	$⊢ ((I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) RingHom (S ↑_{𝑠} ({Base}_{S}^{I}))) \land {Base}_{(I mPoly (S ↾_{𝑠} R))} \in SubRing (I mPoly (S ↾_{𝑠} R))) \to (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}] \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$
23	7 21 22	syl2anc	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (I evalSub S) (R) [{Base}_{(I mPoly (S ↾_{𝑠} R))}] \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$
24	15 23	eqeltrd	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$

Metamath Proof Explorer

Theorem mpfsubrg

Proof