Theorem evlvarval

Description: Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlvarval.1	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
	evlvarval.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
	evlvarval.3	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlvarval.4	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlvarval.5	⊢ ∙ = ( .r ‘ 𝑃 )
	evlvarval.6	⊢ · = ( .r ‘ 𝑆 )
	evlvarval.7	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
	evlvarval.8	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlvarval.9	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
	evlvarval.10	⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
	evlvarval.11	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	evlvarval	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlvarval.1	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2		evlvarval.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
3		evlvarval.3	⊢ 𝐾 = ( Base ‘ 𝑆 )
4		evlvarval.4	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		evlvarval.5	⊢ ∙ = ( .r ‘ 𝑃 )
6		evlvarval.6	⊢ · = ( .r ‘ 𝑆 )
7		evlvarval.7	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
8		evlvarval.8	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evlvarval.9	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
10		evlvarval.10	⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
11		evlvarval.11	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
12	8	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
13	2 10 4 7 12 11	mvrcl	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )
14		fveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
15	1 10 3 7 8 11	evlvar	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑋 ) ) )
16	3	fvexi	⊢ 𝐾 ∈ V
17	16	a1i	⊢ ( 𝜑 → 𝐾 ∈ V )
18	7 17 9	elmaprd	⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐾 )
19	18 11	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐾 )
20	14 15 9 19	fvmptd4	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) )
21	13 20	jca	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )