Theorem evlsvval

Description: Give a formula for the evaluation of a polynomial. (Contributed by SN, 9-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		evlsvval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsvval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		evlsvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5		evlsvval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		evlsvval.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
7		evlsvval.t	⊢ 𝑇 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
8		evlsvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑇 )
9		evlsvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
10		evlsvval.x	⊢ · = ( .r ‘ 𝑇 )
11		evlsvval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐾 ↑m 𝐼 ) × { 𝑥 } ) )
12		evlsvval.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑥 ) ) )
13		evlsvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
14		evlsvval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
15		evlsvval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
16		evlsvval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
17		fveq1	⊢ ( 𝑝 = 𝐴 → ( 𝑝 ‘ 𝑏 ) = ( 𝐴 ‘ 𝑏 ) )
18	17	fveq2d	⊢ ( 𝑝 = 𝐴 → ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) )
19	18	oveq1d	⊢ ( 𝑝 = 𝐴 → ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
20	19	mpteq2dv	⊢ ( 𝑝 = 𝐴 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) )
21	20	oveq2d	⊢ ( 𝑝 = 𝐴 → ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
22		eqid	⊢ ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) = ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
23	1 2 3 4 5 6 7 8 9 10 22 11 12 13 14 15	evlsval3	⊢ ( 𝜑 → 𝑄 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ) )
24		ovexd	⊢ ( 𝜑 → ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ∈ V )
25	21 23 16 24	fvmptd4	⊢ ( 𝜑 → ( 𝑄 ‘ 𝐴 ) = ( 𝑇 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝐴 ‘ 𝑏 ) ) · ( 𝑀 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )