Theorem extvval

Description: Value of the "variable extension" function. (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$$
	extvval.j	$$⊢J=I\setminus \left\{a\right\}$$
	extvval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
Assertion	extvval	Could not format assertion : No typesetting found for |- ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .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		extvval.j	$$⊢J=I\setminus \left\{a\right\}$$
6		extvval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
7		df-extv	Could not format extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) : No typesetting found for |- extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) with typecode |-
8	7	a1i	Could not format ( ph -> extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) ) with typecode |-
9		simpl	$$⊢\left(i=I\wedge r=R\right)\to i=I$$
10		difeq1	$$⊢i=I\to i\setminus \left\{a\right\}=I\setminus \left\{a\right\}$$
11	10 5	eqtr4di	$$⊢i=I\to i\setminus \left\{a\right\}=J$$
12	11	adantr	$$⊢\left(i=I\wedge r=R\right)\to i\setminus \left\{a\right\}=J$$
13		simpr	$$⊢\left(i=I\wedge r=R\right)\to r=R$$
14	12 13	oveq12d	$$⊢\left(i=I\wedge r=R\right)\to \left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r=J\mathrm{mPoly}R$$
15	14	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
16	15 6	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}=M$$
17		oveq2	$$⊢i=I\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
18	17	rabeqdv	$$⊢i=I\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
19	18 1	eqtr4di	$$⊢i=I\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=D$$
20	19	adantr	$$⊢\left(i=I\wedge r=R\right)\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=D$$
21	10	reseq2d	$$⊢i=I\to {x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}={x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}$$
22	21	fveq2d	$$⊢i=I\to f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right)=f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right)$$
23	22	adantr	$$⊢\left(i=I\wedge r=R\right)\to f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right)=f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right)$$
24		fveq2	$$⊢r=R\to 0_r=0_R$$
25	24	adantl	$$⊢\left(i=I\wedge r=R\right)\to 0_r=0_R$$
26	25 2	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to 0_r=\underset{\dot{}}{0}$$
27	23 26	ifeq12d	$$⊢\left(i=I\wedge r=R\right)\to if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)=if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(I\setminus \left\{a\right\}\right)}\right),\underset{\dot{}}{0}\right)$$
28	20 27	mpteq12dv	$$⊢\left(i=I\wedge r=R\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)\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)$$
29	16 28	mpteq12dv	$$⊢\left(i=I\wedge r=R\right)\to \left(f\in {\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)\right)\right)=\left(f\in M⟼\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)$$
30	9 29	mpteq12dv	$$⊢\left(i=I\wedge r=R\right)\to \left(a\in i⟼\left(f\in {\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)\right)\right)\right)=\left(a\in I⟼\left(f\in M⟼\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)\right)$$
31	30	adantl	$$⊢\left(\phi \wedge \left(i=I\wedge r=R\right)\right)\to \left(a\in i⟼\left(f\in {\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)\right)\right)\right)=\left(a\in I⟼\left(f\in M⟼\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)\right)$$
32	3	elexd	$$⊢\phi \to I\in \mathrm{V}$$
33	4	elexd	$$⊢\phi \to R\in \mathrm{V}$$
34	3	mptexd	$$⊢\phi \to \left(a\in I⟼\left(f\in M⟼\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)\right)\in \mathrm{V}$$
35	8 31 32 33 34	ovmpod	Could not format ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( 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. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) with typecode |-