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. ) )

Metamath Proof Explorer

Theorem extvfvv

Proof