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