Theorem extvfv

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=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	extvval.1	$$⊢\underset{\dot{}}{0}=0_R$$
	extvval.i	$$⊢\phi \to I\in V$$
	extvval.r	$$⊢\phi \to R\in W$$
	extvfval.a	$$⊢\phi \to A\in I$$
	extvfval.j	$$⊢J=I\setminus \left\{A\right\}$$
	extvfval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
	extvfv.1	$$⊢\phi \to F\in M$$
Assertion	extvfv	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		extvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		extvval.1	$$⊢\underset{\dot{}}{0}=0_R$$
3		extvval.i	$$⊢\phi \to I\in V$$
4		extvval.r	$$⊢\phi \to R\in W$$
5		extvfval.a	$$⊢\phi \to A\in I$$
6		extvfval.j	$$⊢J=I\setminus \left\{A\right\}$$
7		extvfval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
8		extvfv.1	$$⊢\phi \to F\in M$$
9		fveq1	$$⊢f=F\to f\left({x\upharpoonright }_J\right)=F\left({x\upharpoonright }_J\right)$$
10	9	ifeq1d	$$⊢f=F\to if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)=if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)$$
11	10	mpteq2dv	$$⊢f=F\to \left(x\in D⟼if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)=\left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)$$
12	1 2 3 4 5 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 |-
13		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
14	1 13	rabex2	$$⊢D\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to D\in \mathrm{V}$$
16	15	mptexd	$$⊢\phi \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}$$
17	11 12 8 16	fvmptd4	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) with typecode |-