Theorem evlsrhm

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

	Ref	Expression
Hypotheses	evlsrhm.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsrhm.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
	evlsrhm.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsrhm.t	⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
	evlsrhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		evlsrhm.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsrhm.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3		evlsrhm.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evlsrhm.t	⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
5		evlsrhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
6		eqid	⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 )
7		eqid	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
8		eqid	⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
9		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) )
10	1 2 6 3 4 5 7 8 9	evlsval2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) ∧ ( ( 𝑄 ∘ ( algSc ‘ 𝑊 ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) ) ) )
11	10	simpld	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )