# Metamath Proof Explorer

## 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 ( PwSer1𝑈 ) = ( PwSer1𝑈 )
25 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
26 5 24 25 ply1bas ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
27 26 a1i ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
28 eqid ( +g𝑊 ) = ( +g𝑊 )
29 5 18 28 ply1plusg ( +g𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) )
30 29 a1i ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( +g𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) ) )
31 30 oveqdr ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
32 eqidd ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑆s ( 𝐵m 1o ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆s ( 𝐵m 1o ) ) ) 𝑦 ) )
33 eqid ( .r𝑊 ) = ( .r𝑊 )
34 5 18 33 ply1mulr ( .r𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) )
35 34 a1i ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( .r𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) ) )
36 35 oveqdr ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
37 eqidd ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝑆s ( 𝐵m 1o ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑆s ( 𝐵m 1o ) ) ) 𝑦 ) )
38 22 23 27 23 31 32 36 37 rhmpropd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑊 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) = ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆s ( 𝐵m 1o ) ) ) )
39 21 38 eleqtrrd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) )
40 rhmco ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑆s ( 𝐵m 1o ) ) RingHom 𝑇 ) ∧ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
41 15 39 40 syl2an2r ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
42 13 41 eqeltrd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )