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 𝑇 ) )