evlsrhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015)

	Ref	Expression
Hypotheses	evlsrhm.q	$⊢ Q = (I evalSub S) (R)$
	evlsrhm.w	$⊢ W = I mPoly U$
	evlsrhm.u	$⊢ U = S ↾_{𝑠} R$
	evlsrhm.t	$⊢ T = S ↑_{𝑠} (B^{I})$
	evlsrhm.b	$⊢ B = {Base}_{S}$
Assertion	evlsrhm	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom T)$

Step	Hyp	Ref	Expression
1		evlsrhm.q	$⊢ Q = (I evalSub S) (R)$
2		evlsrhm.w	$⊢ W = I mPoly U$
3		evlsrhm.u	$⊢ U = S ↾_{𝑠} R$
4		evlsrhm.t	$⊢ T = S ↑_{𝑠} (B^{I})$
5		evlsrhm.b	$⊢ B = {Base}_{S}$
6		eqid	$⊢ I mVar U = I mVar U$
7		eqid	$⊢ algSc (W) = algSc (W)$
8		eqid	$⊢ (x \in R ⟼ (B^{I}) \times \{x\}) = (x \in R ⟼ (B^{I}) \times \{x\})$
9		eqid	$⊢ (x \in I ⟼ (y \in (B^{I}) ⟼ y (x))) = (x \in I ⟼ (y \in (B^{I}) ⟼ y (x)))$
10	1 2 6 3 4 5 7 8 9	evlsval2	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to (Q \in (W RingHom T) \land (Q \circ algSc (W) = (x \in R ⟼ (B^{I}) \times \{x\}) \land Q \circ (I mVar U) = (x \in I ⟼ (y \in (B^{I}) ⟼ y (x)))))$
11	10	simpld	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom T)$

Metamath Proof Explorer