Theorem extvfvv

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 )
	extvfvv.1	|- ( ph -> X e. D )
Assertion	extvfvv	|- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = 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		extvfvv.1	|- ( ph -> X e. D )
10		fveq1	|- ( x = X -> ( x ` A ) = ( X ` A ) )
11	10	eqeq1d	|- ( x = X -> ( ( x ` A ) = 0 <-> ( X ` A ) = 0 ) )
12		reseq1	|- ( x = X -> ( x |` J ) = ( X |` J ) )
13	12	fveq2d	|- ( x = X -> ( F ` ( x |` J ) ) = ( F ` ( X |` J ) ) )
14	11 13	ifbieq1d	|- ( x = X -> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) )
15	1 2 3 4 5 6 7 8	extvfv	|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )
16		fvexd	|- ( ph -> ( F ` ( X |` J ) ) e. _V )
17	2	fvexi	|- .0. e. _V
18	17	a1i	|- ( ph -> .0. e. _V )
19	16 18	ifcld	|- ( ph -> if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) e. _V )
20	14 15 9 19	fvmptd4	|- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) )