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

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 ffvelcdmd ⊢ ( ( 𝑆 ∈ 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 × { 𝑦 } ) ) ) )