# Metamath Proof Explorer

## Theorem evl1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015) (Proof shortened by AV, 13-Sep-2019)

Ref Expression
Hypotheses evl1rhm.q 𝑂 = ( eval1𝑅 )
evl1rhm.w 𝑃 = ( Poly1𝑅 )
evl1rhm.t 𝑇 = ( 𝑅s 𝐵 )
evl1rhm.b 𝐵 = ( Base ‘ 𝑅 )
Assertion evl1rhm ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom 𝑇 ) )

### Proof

Step Hyp Ref Expression
1 evl1rhm.q 𝑂 = ( eval1𝑅 )
2 evl1rhm.w 𝑃 = ( Poly1𝑅 )
3 evl1rhm.t 𝑇 = ( 𝑅s 𝐵 )
4 evl1rhm.b 𝐵 = ( Base ‘ 𝑅 )
5 eqid ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
6 1 5 4 evl1fval 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) )
7 eqid ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
8 4 3 7 evls1rhmlem ( 𝑅 ∈ CRing → ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑅s ( 𝐵m 1o ) ) RingHom 𝑇 ) )
9 1on 1o ∈ On
10 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
11 eqid ( 𝑅s ( 𝐵m 1o ) ) = ( 𝑅s ( 𝐵m 1o ) )
12 5 4 10 11 evlrhm ( ( 1o ∈ On ∧ 𝑅 ∈ CRing ) → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
13 9 12 mpan ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) ∈ ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
14 eqidd ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
15 eqidd ( 𝑅 ∈ CRing → ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) = ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
16 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
17 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
18 2 16 17 ply1bas ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
19 18 a1i ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
20 eqid ( +g𝑃 ) = ( +g𝑃 )
21 2 10 20 ply1plusg ( +g𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
22 21 a1i ( 𝑅 ∈ CRing → ( +g𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
23 22 oveqdr ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
24 eqidd ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅s ( 𝐵m 1o ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑅s ( 𝐵m 1o ) ) ) 𝑦 ) )
25 eqid ( .r𝑃 ) = ( .r𝑃 )
26 2 10 25 ply1mulr ( .r𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
27 26 a1i ( 𝑅 ∈ CRing → ( .r𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) ) )
28 27 oveqdr ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
29 eqidd ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝑅s ( 𝐵m 1o ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑅s ( 𝐵m 1o ) ) ) 𝑦 ) )
30 14 15 19 15 23 24 28 29 rhmpropd ( 𝑅 ∈ CRing → ( 𝑃 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) = ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
31 13 30 eleqtrrd ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) ∈ ( 𝑃 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
32 rhmco ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑅s ( 𝐵m 1o ) ) RingHom 𝑇 ) ∧ ( 1o eval 𝑅 ) ∈ ( 𝑃 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) ∈ ( 𝑃 RingHom 𝑇 ) )
33 8 31 32 syl2anc ( 𝑅 ∈ CRing → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) ∈ ( 𝑃 RingHom 𝑇 ) )
34 6 33 eqeltrid ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom 𝑇 ) )