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 ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17 2 16 ply1bas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
18 17 a1i ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
19 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
20 2 10 19 ply1plusg ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
21 20 a1i ⊢ ( 𝑅 ∈ CRing → ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
22 21 oveqdr ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
23 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
24 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
25 2 10 24 ply1mulr ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
26 25 a1i ⊢ ( 𝑅 ∈ CRing → ( .r ‘ 𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) ) )
27 26 oveqdr ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑅 ) ) 𝑦 ) )
28 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
29 14 15 18 15 22 23 27 28 rhmpropd ⊢ ( 𝑅 ∈ CRing → ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) = ( ( 1o mPoly 𝑅 ) RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
30 13 29 eleqtrrd ⊢ ( 𝑅 ∈ CRing → ( 1o eval 𝑅 ) ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
31 rhmco ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) ∧ ( 1o eval 𝑅 ) ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) ∈ ( 𝑃 RingHom 𝑇 ) )
32 8 30 31 syl2anc ⊢ ( 𝑅 ∈ CRing → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) ∈ ( 𝑃 RingHom 𝑇 ) )
33 6 32 eqeltrid ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom 𝑇 ) )