# Metamath Proof Explorer

## Theorem evls1val

Description: Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019)

Ref Expression
Hypotheses evls1fval.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1fval.e 𝐸 = ( 1o evalSub 𝑆 )
evls1fval.b 𝐵 = ( Base ‘ 𝑆 )
evls1val.m 𝑀 = ( 1o mPoly ( 𝑆s 𝑅 ) )
evls1val.k 𝐾 = ( Base ‘ 𝑀 )
Assertion evls1val ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) = ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )

### Proof

Step Hyp Ref Expression
1 evls1fval.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1fval.e 𝐸 = ( 1o evalSub 𝑆 )
3 evls1fval.b 𝐵 = ( Base ‘ 𝑆 )
4 evls1val.m 𝑀 = ( 1o mPoly ( 𝑆s 𝑅 ) )
5 evls1val.k 𝐾 = ( Base ‘ 𝑀 )
6 3 subrgss ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅𝐵 )
7 6 adantl ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅𝐵 )
8 elpwg ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵𝑅𝐵 ) )
9 8 adantl ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑅 ∈ 𝒫 𝐵𝑅𝐵 ) )
10 7 9 mpbird ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ 𝒫 𝐵 )
11 1 2 3 evls1fval ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
12 10 11 syldan ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) )
13 12 fveq1d ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄𝐴 ) = ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ‘ 𝐴 ) )
14 13 3adant3 ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) = ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ‘ 𝐴 ) )
15 1on 1o ∈ On
16 simp1 ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → 𝑆 ∈ CRing )
17 simp2 ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
18 2 fveq1i ( 𝐸𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
19 eqid ( 𝑆s 𝑅 ) = ( 𝑆s 𝑅 )
20 eqid ( 𝑆s ( 𝐵m 1o ) ) = ( 𝑆s ( 𝐵m 1o ) )
21 18 4 19 20 3 evlsrhm ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐸𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) )
22 15 16 17 21 mp3an2i ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝐸𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) )
23 eqid ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) = ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) )
24 5 23 rhmf ( ( 𝐸𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆s ( 𝐵m 1o ) ) ) → ( 𝐸𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) )
25 22 24 syl ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝐸𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) )
26 simp3 ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → 𝐴𝐾 )
27 fvco3 ( ( ( 𝐸𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) ∧ 𝐴𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸𝑅 ) ‘ 𝐴 ) ) )
28 25 26 27 syl2anc ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸𝑅 ) ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸𝑅 ) ‘ 𝐴 ) ) )
29 25 26 ffvelrnd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∈ ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) )
30 ovex ( 𝐵m 1o ) ∈ V
31 20 3 pwsbas ( ( 𝑆 ∈ CRing ∧ ( 𝐵m 1o ) ∈ V ) → ( 𝐵m ( 𝐵m 1o ) ) = ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) )
32 16 30 31 sylancl ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝐵m ( 𝐵m 1o ) ) = ( Base ‘ ( 𝑆s ( 𝐵m 1o ) ) ) )
33 29 32 eleqtrrd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∈ ( 𝐵m ( 𝐵m 1o ) ) )
34 coeq1 ( 𝑥 = ( ( 𝐸𝑅 ) ‘ 𝐴 ) → ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
35 eqid ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
36 fvex ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∈ V
37 3 fvexi 𝐵 ∈ V
38 37 mptex ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V
39 36 38 coex ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V
40 34 35 39 fvmpt ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∈ ( 𝐵m ( 𝐵m 1o ) ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸𝑅 ) ‘ 𝐴 ) ) = ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
41 33 40 syl ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸𝑅 ) ‘ 𝐴 ) ) = ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
42 14 28 41 3eqtrd ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) = ( ( ( 𝐸𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )