Theorem extvfvvcl

Description: Closure for 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	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$$
	extvfvvcl.f	$$⊢\phi \to F\in M$$
	extvfvvcl.x	$$⊢\phi \to X\in D$$
Assertion	extvfvvcl	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) 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		extvfvvcl.f	$$⊢\phi \to F\in M$$
10		extvfvvcl.x	$$⊢\phi \to X\in D$$
11	1 2 3 4 8 6 7 9 10	extvfvv	Could not format ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) with typecode |-
12		eqid	$$⊢J\mathrm{mPoly}R=J\mathrm{mPoly}R$$
13		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
14	13	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^J\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15	12 5 7 14 9	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}⟶B$$
16		breq1	$$⊢h={X\upharpoonright }_J\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left({X\upharpoonright }_J\right)\right)\right)$$
17	1	ssrab3	$$⊢D\subseteq {{\mathbb{N}}_0}^I$$
18	17 10	sselid	$$⊢\phi \to X\in \left({{\mathbb{N}}_0}^I\right)$$
19		difssd	$$⊢\phi \to I\setminus \left\{A\right\}\subseteq I$$
20	6 19	eqsstrid	$$⊢\phi \to J\subseteq I$$
21	18 20	elmapssresd	$$⊢\phi \to {X\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)$$
22		breq1	$$⊢h=X\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(X\right)\right)$$
23	10 1	eleqtrdi	$$⊢\phi \to X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
24	22 23	elrabrd	$$⊢\phi \to {finSupp}_0\left(X\right)$$
25		c0ex	$$⊢0\in \mathrm{V}$$
26	25	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
27	24 26	fsuppres	$$⊢\phi \to {finSupp}_0\left(\left({X\upharpoonright }_J\right)\right)$$
28	16 21 27	elrabd	$$⊢\phi \to {X\upharpoonright }_J\in \left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
29	15 28	ffvelcdmd	$$⊢\phi \to F\left({X\upharpoonright }_J\right)\in B$$
30	5 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
31	4 30	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
32	29 31	ifcld	$$⊢\phi \to if\left(X\left(A\right)=0,F\left({X\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\in B$$
33	11 32	eqeltrd	Could not format ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) with typecode |-