Definition df-extv

Description: Define the "variable extension" function. The function ( ( I extendVars R )A ) converts polynomials with variables indexed by ( I \ { A } ) into polynomials indexed by I , and therefore maps elements of ( ( I \ { A } ) mPoly R ) onto ( I mPoly R ) . (Contributed by Thierry Arnoux, 20-Jan-2026)

	Ref	Expression
Assertion	df-extv	Could not format assertion : 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 |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cextv	Could not format extendVars : No typesetting found for class extendVars with typecode class
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		va	$$setvara$$
5	1	cv	$$setvari$$
6		vf	$$setvarf$$
7		cbs	$$class\mathrm{Base}$$
8	4	cv	$$setvara$$
9	8	csn	$$class\left\{a\right\}$$
10	5 9	cdif	$$class\left(i\setminus \left\{a\right\}\right)$$
11		cmpl	$$class\mathrm{mPoly}$$
12	3	cv	$$setvarr$$
13	10 12 11	co	$$class\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)$$
14	13 7	cfv	$$class{\mathrm{Base}}_{\left(\left(i\setminus \left\{a\right\}\right)\mathrm{mPoly}r\right)}$$
15		vx	$$setvarx$$
16		vh	$$setvarh$$
17		cn0	$$class{\mathbb{N}}_0$$
18		cmap	$$class{\uparrow }_{𝑚}$$
19	17 5 18	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
20	16	cv	$$setvarh$$
21		cfsupp	$$class\mathrm{finSupp}$$
22		cc0	$$class0$$
23	20 22 21	wbr	$$wff{finSupp}_0\left(h\right)$$
24	23 16 19	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}$$
25	15	cv	$$setvarx$$
26	8 25	cfv	$$classx\left(a\right)$$
27	26 22	wceq	$$wffx\left(a\right)=0$$
28	6	cv	$$setvarf$$
29	25 10	cres	$$class\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right)$$
30	29 28	cfv	$$classf\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right)$$
31		c0g	$$class{0}_{𝑔}$$
32	12 31	cfv	$$class{0}_r$$
33	27 30 32	cif	$$classif\left(x\left(a\right)=0,f\left({x\upharpoonright }_{\left(i\setminus \left\{a\right\}\right)}\right),0_r\right)$$
34	15 24 33	cmpt	$$class\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)$$
35	6 14 34	cmpt	$$class\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)$$
36	4 5 35	cmpt	$$class\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)$$
37	1 3 2 2 36	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼\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)\right)$$
38	0 37	wceq	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 wff 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 wff