Theorem extvfvalf

Description: The "variable extension" function maps polynomials with variables indexed in J to polynomials with variables indexed in I . (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	extvfvvcl.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
	extvfvvcl.3	|- .0. = ( 0g ` R )
	extvfvvcl.i	|- ( ph -> I e. V )
	extvfvvcl.r	|- ( ph -> R e. Ring )
	extvfvvcl.b	|- B = ( Base ` R )
	extvfvvcl.j	|- J = ( I \ { A } )
	extvfvvcl.m	|- M = ( Base ` ( J mPoly R ) )
	extvfvvcl.1	|- ( ph -> A e. I )
	extvfvalf.n	|- N = ( Base ` ( I mPoly R ) )
Assertion	extvfvalf	|- ( ph -> ( ( I extendVars R ) ` A ) : M --> N )

Proof

Step	Hyp	Ref	Expression
1		extvfvvcl.d	|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2		extvfvvcl.3	|- .0. = ( 0g ` R )
3		extvfvvcl.i	|- ( ph -> I e. V )
4		extvfvvcl.r	|- ( ph -> R e. Ring )
5		extvfvvcl.b	|- B = ( Base ` R )
6		extvfvvcl.j	|- J = ( I \ { A } )
7		extvfvvcl.m	|- M = ( Base ` ( J mPoly R ) )
8		extvfvvcl.1	|- ( ph -> A e. I )
9		extvfvalf.n	|- N = ( Base ` ( I mPoly R ) )
10		ovex	|- ( NN0 ^m I ) e. _V
11	1 10	rabex2	|- D e. _V
12	11	a1i	|- ( ( ph /\ f e. M ) -> D e. _V )
13	12	mptexd	|- ( ( ph /\ f e. M ) -> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) e. _V )
14	1 2 3 4 8 6 7	extvfval	|- ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) )
15	3	adantr	|- ( ( ph /\ f e. M ) -> I e. V )
16	4	adantr	|- ( ( ph /\ f e. M ) -> R e. Ring )
17	8	adantr	|- ( ( ph /\ f e. M ) -> A e. I )
18		simpr	|- ( ( ph /\ f e. M ) -> f e. M )
19	1 2 15 16 5 6 7 17 18 9	extvfvcl	|- ( ( ph /\ f e. M ) -> ( ( ( I extendVars R ) ` A ) ` f ) e. N )
20	13 14 19	fmpt2d	|- ( ph -> ( ( I extendVars R ) ` A ) : M --> N )