Theorem evls1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019)

	Ref	Expression
Hypotheses	evls1rhm.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1rhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1rhm.t	⊢ 𝑇 = ( 𝑆 ↑s 𝐵 )
	evls1rhm.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1rhm.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
Assertion	evls1rhm	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		evls1rhm.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1rhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		evls1rhm.t	⊢ 𝑇 = ( 𝑆 ↑s 𝐵 )
4		evls1rhm.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		evls1rhm.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
6	2	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
7	6	adantl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ⊆ 𝐵 )
8		elpwg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
9	8	adantl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
10	7 9	mpbird	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ 𝒫 𝐵 )
11		eqid	⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
12	1 11 2	evls1fval	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
13	10 12	syldan	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
14		eqid	⊢ ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
15	2 3 14	evls1rhmlem	⊢ ( 𝑆 ∈ CRing → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) )
16		1on	⊢ 1o ∈ On
17		eqid	⊢ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
18		eqid	⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
19		eqid	⊢ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 1o ) )
20	17 18 4 19 2	evlsrhm	⊢ ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
21	16 20	mp3an1	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
22		eqidd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
23		eqidd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
24		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25	5 24	ply1bas	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
26	25	a1i	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
27		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
28	5 18 27	ply1plusg	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) )
29	28	a1i	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( +g ‘ 𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) ) )
30	29	oveqdr	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
31		eqidd	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
32		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
33	5 18 32	ply1mulr	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) )
34	33	a1i	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( .r ‘ 𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) ) )
35	34	oveqdr	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
36		eqidd	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
37	22 23 26 23 30 31 35 36	rhmpropd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
38	21 37	eleqtrrd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
39		rhmco	⊢ ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) ∧ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
40	15 38 39	syl2an2r	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
41	13 40	eqeltrd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )