Theorem evlrhm

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

	Ref	Expression
Hypotheses	evlval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evlval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evlrhm.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
	evlrhm.t	⊢ 𝑇 = ( 𝑅 ↑s ( 𝐵 ↑m 𝐼 ) )
Assertion	evlrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		evlval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2		evlval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		evlrhm.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
4		evlrhm.t	⊢ 𝑇 = ( 𝑅 ↑s ( 𝐵 ↑m 𝐼 ) )
5		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6	5	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
7	2	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
8	6 7	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
9	1 2	evlval	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )
10		eqid	⊢ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) )
11		eqid	⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
12	9 10 11 4 2	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑄 ∈ ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) )
13	8 12	mpd3an3	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) )
14	2	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
15	14	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
16	15	oveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly 𝑅 ) )
17	16 3	eqtr4di	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = 𝑊 )
18	17	oveq1d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) = ( 𝑊 RingHom 𝑇 ) )
19	13 18	eleqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )