evlrhm

Description: The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	evlval.q	$⊢ Q = I eval R$
	evlval.b	$⊢ B = {Base}_{R}$
	evlrhm.w	$⊢ W = I mPoly R$
	evlrhm.t	$⊢ T = R ↑_{𝑠} (B^{I})$
Assertion	evlrhm	$⊢ (I \in V \land R \in CRing) \to Q \in (W RingHom T)$

Step	Hyp	Ref	Expression
1		evlval.q	$⊢ Q = I eval R$
2		evlval.b	$⊢ B = {Base}_{R}$
3		evlrhm.w	$⊢ W = I mPoly R$
4		evlrhm.t	$⊢ T = R ↑_{𝑠} (B^{I})$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	5	adantl	$⊢ (I \in V \land R \in CRing) \to R \in Ring$
7	2	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
8	6 7	syl	$⊢ (I \in V \land R \in CRing) \to B \in SubRing (R)$
9	1 2	evlval	$⊢ Q = (I evalSub R) (B)$
10		eqid	$⊢ I mPoly (R ↾_{𝑠} B) = I mPoly (R ↾_{𝑠} B)$
11		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
12	9 10 11 4 2	evlsrhm	$⊢ (I \in V \land R \in CRing \land B \in SubRing (R)) \to Q \in ((I mPoly (R ↾_{𝑠} B)) RingHom T)$
13	8 12	mpd3an3	$⊢ (I \in V \land R \in CRing) \to Q \in ((I mPoly (R ↾_{𝑠} B)) RingHom T)$
14	2	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
15	14	adantl	$⊢ (I \in V \land R \in CRing) \to R ↾_{𝑠} B = R$
16	15	oveq2d	$⊢ (I \in V \land R \in CRing) \to I mPoly (R ↾_{𝑠} B) = I mPoly R$
17	16 3	eqtr4di	$⊢ (I \in V \land R \in CRing) \to I mPoly (R ↾_{𝑠} B) = W$
18	17	oveq1d	$⊢ (I \in V \land R \in CRing) \to (I mPoly (R ↾_{𝑠} B)) RingHom T = W RingHom T$
19	13 18	eleqtrd	$⊢ (I \in V \land R \in CRing) \to Q \in (W RingHom T)$

Metamath Proof Explorer