Metamath Proof Explorer

Theorem evlsval3

Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses evlsval3.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsval3.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
evlsval3.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlsval3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlsval3.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsval3.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsval3.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
evlsval3.m ⊢ 𝑀 = ( mulGrp ‘ 𝑇 )
evlsval3.w ⊢ ↑ = ( .g ‘ 𝑀 )
evlsval3.x ⊢ · = ( .r ‘ 𝑇 )
evlsval3.e ⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
evlsval3.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
evlsval3.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
evlsval3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsval3.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsval3.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion evlsval3 ( 𝜑 → 𝑄 = 𝐸 )

Proof

Step Hyp Ref Expression
1 evlsval3.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsval3.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3 evlsval3.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 evlsval3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5 evlsval3.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 evlsval3.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
7 evlsval3.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
8 evlsval3.m ⊢ 𝑀 = ( mulGrp ‘ 𝑇 )
9 evlsval3.w ⊢ ↑ = ( .g ‘ 𝑀 )
10 evlsval3.x ⊢ · = ( .r ‘ 𝑇 )
11 evlsval3.e ⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
12 evlsval3.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
13 evlsval3.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
14 evlsval3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
15 evlsval3.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
16 evlsval3.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
17 eqid ⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar 𝑈 )
18 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
19 1 2 17 6 7 5 18 12 13 evlsval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) )
20 14 15 16 19 syl3anc ⊢ ( 𝜑 → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) )
21 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
22 6 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
23 15 16 22 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
24 ovexd ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
25 7 pwscrng ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → 𝑇 ∈ CRing )
26 15 24 25 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ CRing )
27 5 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
28 16 27 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
29 28 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) )
30 12 29 eqtr4id ⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) )
31 15 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
32 eqid ⊢ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
33 7 5 32 pwsdiagrhm ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) )
34 31 24 33 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) )
35 6 resrhm ⊢ ( ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) )
36 34 16 35 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) )
37 30 36 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 RingHom 𝑇 ) )
38 5 fvexi ⊢ 𝐾 ∈ V
39 elmapg ⊢ ( ( 𝐾 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↔ 𝑎 : 𝐼 ⟶ 𝐾 ) )
40 38 14 39 sylancr ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↔ 𝑎 : 𝐼 ⟶ 𝐾 ) )
41 40 biimpa ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
42 41 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝐾 )
43 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 )
44 42 43 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ 𝐾 )
45 44 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
46 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ↑m 𝐼 ) ∈ V )
47 7 5 21 pwselbasb ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐾 ↑m 𝐼 ) ∈ V ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 ) )
48 15 46 47 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 ) )
49 45 48 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) )
50 49 13 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ ( Base ‘ 𝑇 ) )
51 2 3 21 4 8 9 10 17 11 14 23 26 37 50 18 evlslem1 ⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) ∧ ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) )
52 51 simp2d ⊢ ( 𝜑 → ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 )
53 51 simp3d ⊢ ( 𝜑 → ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 )
54 51 simp1d ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) )
55 2 21 18 17 14 23 26 37 50 evlseu ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) )
56 coeq1 ⊢ ( 𝑓 = 𝐸 → ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) )
57 56 eqeq1d ⊢ ( 𝑓 = 𝐸 → ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ↔ ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ) )
58 coeq1 ⊢ ( 𝑓 = 𝐸 → ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) )
59 58 eqeq1d ⊢ ( 𝑓 = 𝐸 → ( ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ↔ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) )
60 57 59 anbi12d ⊢ ( 𝑓 = 𝐸 → ( ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) )
61 60 riota2 ⊢ ( ( 𝐸 ∈ ( 𝑃 RingHom 𝑇 ) ∧ ∃! 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) → ( ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 ) )
62 54 55 61 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐸 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝐸 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ↔ ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 ) )
63 52 53 62 mpbi2and ⊢ ( 𝜑 → ( ℩ 𝑓 ∈ ( 𝑃 RingHom 𝑇 ) ( ( 𝑓 ∘ ( algSc ‘ 𝑃 ) ) = 𝐹 ∧ ( 𝑓 ∘ ( 𝐼 mVar 𝑈 ) ) = 𝐺 ) ) = 𝐸 )
64 20 63 eqtrd ⊢ ( 𝜑 → 𝑄 = 𝐸 )