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 )

Metamath Proof Explorer

Theorem extvfvalf

Proof