Theorem evlvarval

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

	Ref	Expression
Hypotheses	evlvarval.1	|- Q = ( I eval S )
	evlvarval.2	|- P = ( I mPoly S )
	evlvarval.3	|- K = ( Base ` S )
	evlvarval.4	|- B = ( Base ` P )
	evlvarval.5	|- .xb = ( .r ` P )
	evlvarval.6	|- .x. = ( .r ` S )
	evlvarval.7	|- ( ph -> I e. Z )
	evlvarval.8	|- ( ph -> S e. CRing )
	evlvarval.9	|- ( ph -> A e. ( K ^m I ) )
	evlvarval.10	|- V = ( I mVar S )
	evlvarval.11	|- ( ph -> X e. I )
Assertion	evlvarval	|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlvarval.1	|- Q = ( I eval S )
2		evlvarval.2	|- P = ( I mPoly S )
3		evlvarval.3	|- K = ( Base ` S )
4		evlvarval.4	|- B = ( Base ` P )
5		evlvarval.5	|- .xb = ( .r ` P )
6		evlvarval.6	|- .x. = ( .r ` S )
7		evlvarval.7	|- ( ph -> I e. Z )
8		evlvarval.8	|- ( ph -> S e. CRing )
9		evlvarval.9	|- ( ph -> A e. ( K ^m I ) )
10		evlvarval.10	|- V = ( I mVar S )
11		evlvarval.11	|- ( ph -> X e. I )
12	8	crngringd	|- ( ph -> S e. Ring )
13	2 10 4 7 12 11	mvrcl	|- ( ph -> ( V ` X ) e. B )
14		fveq1	|- ( a = A -> ( a ` X ) = ( A ` X ) )
15	1 10 3 7 8 11	evlvar	|- ( ph -> ( Q ` ( V ` X ) ) = ( a e. ( K ^m I ) |-> ( a ` X ) ) )
16	3	fvexi	|- K e. _V
17	16	a1i	|- ( ph -> K e. _V )
18	7 17 9	elmaprd	|- ( ph -> A : I --> K )
19	18 11	ffvelcdmd	|- ( ph -> ( A ` X ) e. K )
20	14 15 9 19	fvmptd4	|- ( ph -> ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) )
21	13 20	jca	|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )