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		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
19	3	difexd	$$⊢\phi \to I\setminus \left\{A\right\}\in \mathrm{V}$$
20	6 19	eqeltrid	$$⊢\phi \to J\in \mathrm{V}$$
21	1	ssrab3	$$⊢D\subseteq {{\mathbb{N}}_0}^I$$
22	21 10	sselid	$$⊢\phi \to X\in \left({{\mathbb{N}}_0}^I\right)$$
23	3 18 22	elmaprd	$$⊢\phi \to X:I⟶{\mathbb{N}}_0$$
24		difssd	$$⊢\phi \to I\setminus \left\{A\right\}\subseteq I$$
25	6 24	eqsstrid	$$⊢\phi \to J\subseteq I$$
26	23 25	fssresd	$$⊢\phi \to \left({X\upharpoonright }_J\right):J⟶{\mathbb{N}}_0$$
27	18 20 26	elmapdd	$$⊢\phi \to {X\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)$$
28		breq1	$$⊢h=X\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(X\right)\right)$$
29	10 1	eleqtrdi	$$⊢\phi \to X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
30	28 29	elrabrd	$$⊢\phi \to {finSupp}_0\left(X\right)$$
31		c0ex	$$⊢0\in \mathrm{V}$$
32	31	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
33	30 32	fsuppres	$$⊢\phi \to {finSupp}_0\left(\left({X\upharpoonright }_J\right)\right)$$
34	16 27 33	elrabd	$$⊢\phi \to {X\upharpoonright }_J\in \left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
35	15 34	ffvelcdmd	$$⊢\phi \to F\left({X\upharpoonright }_J\right)\in B$$
36	5 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
37	4 36	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
38	35 37	ifcld	$$⊢\phi \to if\left(X\left(A\right)=0,F\left({X\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\in B$$
39	11 38	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 |-