This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evlsrhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015)

Ref Expression
Hypotheses evlsrhm.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsrhm.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsrhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsrhm.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
evlsrhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion evlsrhm ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 evlsrhm.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsrhm.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3 evlsrhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 evlsrhm.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
5 evlsrhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 eqid ⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 )
7 eqid ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
8 eqid ⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
9 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) )
10 1 2 6 3 4 5 7 8 9 evlsval2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) ∧ ( ( 𝑄 ∘ ( algSc ‘ 𝑊 ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑄 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑦 ‘ 𝑥 ) ) ) ) ) )
11 10 simpld ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )