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=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	extvfvvcl.3	$$⊢\underset{\dot{}}{0}=0_R$$
	extvfvvcl.i	$$⊢\phi \to I\in V$$
	extvfvvcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	extvfvvcl.b	$$⊢B={\mathrm{Base}}_R$$
	extvfvvcl.j	$$⊢J=I\setminus \left\{A\right\}$$
	extvfvvcl.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
	extvfvvcl.1	$$⊢\phi \to A\in I$$
	extvfvalf.n	$$⊢N={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
Assertion	extvfvalf	Could not format assertion : No typesetting found for |- ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		extvfvvcl.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		extvfvvcl.3	$$⊢\underset{\dot{}}{0}=0_R$$
3		extvfvvcl.i	$$⊢\phi \to I\in V$$
4		extvfvvcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		extvfvvcl.b	$$⊢B={\mathrm{Base}}_R$$
6		extvfvvcl.j	$$⊢J=I\setminus \left\{A\right\}$$
7		extvfvvcl.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
8		extvfvvcl.1	$$⊢\phi \to A\in I$$
9		extvfvalf.n	$$⊢N={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
10		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
11	1 10	rabex2	$$⊢D\in \mathrm{V}$$
12	11	a1i	$$⊢\left(\phi \wedge f\in M\right)\to D\in \mathrm{V}$$
13	12	mptexd	$$⊢\left(\phi \wedge f\in M\right)\to \left(x\in D⟼if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
14	1 2 3 4 8 6 7	extvfval	Could not format ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) ) : No typesetting found for |- ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M |-> ( x e. D |-> if ( ( x ` A ) = 0 , ( f ` ( x |` J ) ) , .0. ) ) ) ) with typecode |-
15	3	adantr	$$⊢\left(\phi \wedge f\in M\right)\to I\in V$$
16	4	adantr	$$⊢\left(\phi \wedge f\in M\right)\to R\in \mathrm{Ring}$$
17	8	adantr	$$⊢\left(\phi \wedge f\in M\right)\to A\in I$$
18		simpr	$$⊢\left(\phi \wedge f\in M\right)\to f\in M$$
19	1 2 15 16 5 6 7 17 18 9	extvfvcl	Could not format ( ( ph /\ f e. M ) -> ( ( ( I extendVars R ) ` A ) ` f ) e. N ) : No typesetting found for |- ( ( ph /\ f e. M ) -> ( ( ( I extendVars R ) ` A ) ` f ) e. N ) with typecode |-
20	13 14 19	fmpt2d	Could not format ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) : No typesetting found for |- ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) with typecode |-