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

Metamath Proof Explorer

Theorem evls1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019)

Ref Expression
Hypotheses evls1rhm.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1rhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evls1rhm.t ⊢ 𝑇 = ( 𝑆 ↑s 𝐵 )
evls1rhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1rhm.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
Assertion evls1rhm ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 evls1rhm.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1rhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 evls1rhm.t ⊢ 𝑇 = ( 𝑆 ↑s 𝐵 )
4 evls1rhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evls1rhm.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
6 2 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
7 6 adantl ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ⊆ 𝐵 )
8 elpwg ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
9 8 adantl ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
10 7 9 mpbird ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ 𝒫 𝐵 )
11 eqid ⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
12 1 11 2 evls1fval ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
13 10 12 syldan ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) )
14 eqid ⊢ ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
15 2 3 14 evls1rhmlem ⊢ ( 𝑆 ∈ CRing → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) )
16 1on ⊢ 1o ∈ On
17 eqid ⊢ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
18 eqid ⊢ ( 1o mPoly 𝑈 ) = ( 1o mPoly 𝑈 )
19 eqid ⊢ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 1o ) )
20 17 18 4 19 2 evlsrhm ⊢ ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
21 16 20 mp3an1 ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
22 eqidd ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
23 eqidd ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
24 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25 5 24 ply1bas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) )
26 25 a1i ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ ( 1o mPoly 𝑈 ) ) )
27 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
28 5 18 27 ply1plusg ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) )
29 28 a1i ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( +g ‘ 𝑊 ) = ( +g ‘ ( 1o mPoly 𝑈 ) ) )
30 29 oveqdr ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
31 eqidd ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
32 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
33 5 18 32 ply1mulr ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) )
34 33 a1i ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( .r ‘ 𝑊 ) = ( .r ‘ ( 1o mPoly 𝑈 ) ) )
35 34 oveqdr ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 1o mPoly 𝑈 ) ) 𝑦 ) )
36 eqidd ⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) 𝑦 ) )
37 22 23 26 23 30 31 35 36 rhmpropd ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( ( 1o mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
38 21 37 eleqtrrd ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
39 rhmco ⊢ ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) ∧ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( 𝑊 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
40 15 38 39 syl2an2r ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ) ∈ ( 𝑊 RingHom 𝑇 ) )
41 13 40 eqeltrd ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) )