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

Metamath Proof Explorer

Theorem evlrhm

Description: The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evlval.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
evlval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evlrhm.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
evlrhm.t ⊢ 𝑇 = ( 𝑅 ↑s ( 𝐵 ↑m 𝐼 ) )
Assertion evlrhm ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 evlval.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2 evlval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 evlrhm.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
4 evlrhm.t ⊢ 𝑇 = ( 𝑅 ↑s ( 𝐵 ↑m 𝐼 ) )
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
7 2 subrgid ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
8 6 7 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
9 1 2 evlval ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝐵 )
10 eqid ⊢ ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) )
11 eqid ⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
12 9 10 11 4 2 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑄 ∈ ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) )
13 8 12 mpd3an3 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) )
14 2 ressid ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
15 14 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
16 15 oveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 𝐼 mPoly 𝑅 ) )
17 16 3 eqtr4di ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) = 𝑊 )
18 17 oveq1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( ( 𝐼 mPoly ( 𝑅 ↾s 𝐵 ) ) RingHom 𝑇 ) = ( 𝑊 RingHom 𝑇 ) )
19 13 18 eleqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )