Theorem evlvvval

Description: Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025)

	Ref	Expression
Hypotheses	evlvvval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evlvvval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	evlvvval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	evlvvval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	evlvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	evlvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
	evlvvval.x	⊢ · = ( .r ‘ 𝑅 )
	evlvvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlvvval.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evlvvval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	evlvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion	evlvvval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑅 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlvvval.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2		evlvvval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		evlvvval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		evlvvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
5		evlvvval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
6		evlvvval.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
7		evlvvval.w	⊢ ↑ = ( .g ‘ 𝑀 )
8		evlvvval.x	⊢ · = ( .r ‘ 𝑅 )
9		evlvvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10		evlvvval.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
11		evlvvval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
12		evlvvval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
13		eqid	⊢ ( ( 𝐼 evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) = ( ( 𝐼 evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
14		eqid	⊢ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) = ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) )
15		eqid	⊢ ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = ( 𝑅 ↾s ( Base ‘ 𝑅 ) )
16		eqid	⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) )
17	10	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19	18	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
20	17 19	syl	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
21	18	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
22	10 21	syl	⊢ ( 𝜑 → ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) = 𝑅 )
23	22	oveq2d	⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) = ( 𝐼 mPoly 𝑅 ) )
24	23 2	eqtr4di	⊢ ( 𝜑 → ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) = 𝑃 )
25	24	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) = ( Base ‘ 𝑃 ) )
26	25 3	eqtr4di	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) = 𝐵 )
27	11 26	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑅 ↾s ( Base ‘ 𝑅 ) ) ) ) )
28	13 1 14 15 16 9 10 20 27	evlsevl	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) ‘ 𝐹 ) = ( 𝑄 ‘ 𝐹 ) )
29	28	fveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) ‘ 𝐹 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) )
30	13 14 16 15 4 5 6 7 8 9 10 20 27 12	evlsvvval	⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑅 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )
31	29 30	eqtr3d	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑅 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) )