Theorem extvfval

Description: The "variable extension" function evaluated for 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)}$$
Assertion	extvfval	Could not format assertion : 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 |-

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		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
9	8	difeq2d	$$⊢a=A\to I\setminus \left\{a\right\}=I\setminus \left\{A\right\}$$
10	9 6	eqtr4di	$$⊢a=A\to I\setminus \left\{a\right\}=J$$
11	10	fvoveq1d	$$⊢a=A\to {\mathrm{Base}}_{\left(\left(I\setminus \left\{a\right\}\right)\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
12	11 7	eqtr4di	$$⊢a=A\to {\mathrm{Base}}_{\left(\left(I\setminus \left\{a\right\}\right)\mathrm{mPoly}R\right)}=M$$
13		fveqeq2	$$⊢a=A\to \left(x\left(a\right)=0\leftrightarrow x\left(A\right)=0\right)$$
14	10	reseq2d	$$⊢a=A\to {x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}={x\upharpoonright }_J$$
15	14	fveq2d	$$⊢a=A\to f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right)=f\left({x\upharpoonright }_J\right)$$
16	13 15	ifbieq1d	$$⊢a=A\to if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right),\underset{\dot{}}{0}\right)=if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)$$
17	16	mpteq2dv	$$⊢a=A\to \left(x\in D⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\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)$$
18	12 17	mpteq12dv	$$⊢a=A\to \left(f\in {\mathrm{Base}}_{\left(\left(I\setminus \left\{a\right\}\right)\mathrm{mPoly}R\right)}⟼\left(x\in D⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right),\underset{\dot{}}{0}\right)\right)\right)=\left(f\in M⟼\left(x\in D⟼if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\right)$$
19		eqid	$$⊢I\setminus \left\{a\right\}=I\setminus \left\{a\right\}$$
20		eqid	$$⊢{\mathrm{Base}}_{\left(\left(I\setminus \left\{a\right\}\right)\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(\left(I\setminus \left\{a\right\}\right)\mathrm{mPoly}R\right)}$$
21	1 2 3 4 19 20	extvval	Could not format ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) : No typesetting found for |- ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) with typecode |-
22	7	fvexi	$$⊢M\in \mathrm{V}$$
23	22	mptex	$$⊢\left(f\in M⟼\left(x\in D⟼if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
24	23	a1i	$$⊢\phi \to \left(f\in M⟼\left(x\in D⟼if\left(x\left(A\right)=0,f\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
25	18 21 5 24	fvmptd4	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 |-