Theorem extvfv

Description: The "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	extvval.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
	extvval.1	|- .0. = ( 0g ` R )
	extvval.i	|- ( ph -> I e. V )
	extvval.r	|- ( ph -> R e. W )
	extvfval.a	|- ( ph -> A e. I )
	extvfval.j	|- J = ( I \ { A } )
	extvfval.m	|- M = ( Base ` ( J mPoly R ) )
	extvfv.1	|- ( ph -> F e. M )
Assertion	extvfv	|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		extvval.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2		extvval.1	|- .0. = ( 0g ` R )
3		extvval.i	|- ( ph -> I e. V )
4		extvval.r	|- ( ph -> R e. W )
5		extvfval.a	|- ( ph -> A e. I )
6		extvfval.j	|- J = ( I \ { A } )
7		extvfval.m	|- M = ( Base ` ( J mPoly R ) )
8		extvfv.1	|- ( ph -> F e. M )
9		fveq1	|- ( f = F -> ( f ` ( x |` J ) ) = ( F ` ( x |` J ) ) )
10	9	ifeq1d	|- ( f = F -> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) = if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) )
11	10	mpteq2dv	|- ( f = F -> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )
12	1 2 3 4 5 6 7	extvfval	|- ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) )
13		ovex	|- ( NN0 ^m I ) e. _V
14	1 13	rabex2	|- D e. _V
15	14	a1i	|- ( ph -> D e. _V )
16	15	mptexd	|- ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) e. _V )
17	11 12 8 16	fvmptd4	|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )