Theorem extvfvcl

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$$
	extvfvcl.n	$$⊢N={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
Assertion	extvfvcl	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) 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		extvfvcl.n	$$⊢N={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
11	5	fvexi	$$⊢B\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to B\in \mathrm{V}$$
13		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
14	1 13	rabex2	$$⊢D\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to D\in \mathrm{V}$$
16		fvexd	$$⊢\left(\phi \wedge x\in D\right)\to F\left({x\upharpoonright }_J\right)\in \mathrm{V}$$
17	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
18	17	a1i	$$⊢\left(\phi \wedge x\in D\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
19	16 18	ifcld	$$⊢\left(\phi \wedge x\in D\right)\to if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\in \mathrm{V}$$
20	1 2 3 4 8 6 7 9	extvfv	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) with typecode |-
21	3	adantr	$$⊢\left(\phi \wedge x\in D\right)\to I\in V$$
22	4	adantr	$$⊢\left(\phi \wedge x\in D\right)\to R\in \mathrm{Ring}$$
23	8	adantr	$$⊢\left(\phi \wedge x\in D\right)\to A\in I$$
24	9	adantr	$$⊢\left(\phi \wedge x\in D\right)\to F\in M$$
25		simpr	$$⊢\left(\phi \wedge x\in D\right)\to x\in D$$
26	1 2 21 22 5 6 7 23 24 25	extvfvvcl	Could not format ( ( ph /\ x e. D ) -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` x ) e. B ) : No typesetting found for |- ( ( ph /\ x e. D ) -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` x ) e. B ) with typecode |-
27	19 20 26	fmpt2d	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) : D --> B ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) : D --> B ) with typecode |-
28	12 15 27	elmapdd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( B ^m D ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( B ^m D ) ) with typecode |-
29		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
30	1	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
31		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
32	29 5 30 31 3	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}=B^D$$
33	28 32	eleqtrrd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) ) with typecode |-
34	15	mptexd	$$⊢\phi \to \left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
35	17	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
36	19	fmpttd	$$⊢\phi \to \left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right):D⟶\mathrm{V}$$
37	36	ffund	$$⊢\phi \to \mathrm{Fun}\left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)$$
38		fveq1	$$⊢y=x\to y\left(A\right)=x\left(A\right)$$
39	38	eqeq1d	$$⊢y=x\to \left(y\left(A\right)=0\leftrightarrow x\left(A\right)=0\right)$$
40	39	cbvrabv	$$⊢\left\{y\in D|y\left(A\right)=0\right\}=\left\{x\in D|x\left(A\right)=0\right\}$$
41	40	partfun2	$$⊢\left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\cup \left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)$$
42	41	oveq1i	$$⊢\left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}=\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\cup \left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
43	40 15	rabexd	$$⊢\phi \to \left\{y\in D|y\left(A\right)=0\right\}\in \mathrm{V}$$
44	43	mptexd	$$⊢\phi \to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\in \mathrm{V}$$
45	15	difexd	$$⊢\phi \to D\setminus \left\{y\in D|y\left(A\right)=0\right\}\in \mathrm{V}$$
46	45	mptexd	$$⊢\phi \to \left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\in \mathrm{V}$$
47	44 46 35	suppun2	$$⊢\phi \to \left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\cup \left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}={supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\right)\cup {supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\right)$$
48	42 47	eqtrid	$$⊢\phi \to \left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}={supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\right)\cup {supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\right)$$
49		eqid	$$⊢J\mathrm{mPoly}R=J\mathrm{mPoly}R$$
50		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\}$$
51	50	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\}$$
52	49 5 7 51 9	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}⟶B$$
53		breq1	$$⊢h={x\upharpoonright }_J\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left({x\upharpoonright }_J\right)\right)\right)$$
54		ssrab2	$$⊢\left\{y\in D|y\left(A\right)=0\right\}\subseteq D$$
55		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
56	55	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
57	1 56	eqsstrid	$$⊢\phi \to D\subseteq {{\mathbb{N}}_0}^I$$
58	54 57	sstrid	$$⊢\phi \to \left\{y\in D|y\left(A\right)=0\right\}\subseteq {{\mathbb{N}}_0}^I$$
59	58	sselda	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to x\in \left({{\mathbb{N}}_0}^I\right)$$
60		difssd	$$⊢\phi \to I\setminus \left\{A\right\}\subseteq I$$
61	6 60	eqsstrid	$$⊢\phi \to J\subseteq I$$
62	61	adantr	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to J\subseteq I$$
63	59 62	elmapssresd	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to {x\upharpoonright }_J\in \left({{\mathbb{N}}_0}^J\right)$$
64	54	a1i	$$⊢\phi \to \left\{y\in D|y\left(A\right)=0\right\}\subseteq D$$
65	64	sselda	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to x\in D$$
66	30	psrbagfsupp	$$⊢x\in D\to {finSupp}_0\left(x\right)$$
67	65 66	syl	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to {finSupp}_0\left(x\right)$$
68		c0ex	$$⊢0\in \mathrm{V}$$
69	68	a1i	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to 0\in \mathrm{V}$$
70	67 69	fsuppres	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to {finSupp}_0\left(\left({x\upharpoonright }_J\right)\right)$$
71	53 63 70	elrabd	$$⊢\left(\phi \wedge x\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to {x\upharpoonright }_J\in \left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
72	52 71	cofmpt	$$⊢\phi \to F\circ \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)$$
73	72	oveq1d	$$⊢\phi \to \left(F\circ \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
74	43	mptexd	$$⊢\phi \to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\in \mathrm{V}$$
75		suppco	$$⊢\left(F\in M\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\in \mathrm{V}\right)\to \left(F\circ \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}={\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\left[F\mathrm{supp}\underset{\dot{}}{0}\right]$$
76	9 74 75	syl2anc	$$⊢\phi \to \left(F\circ \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}={\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\left[F\mathrm{supp}\underset{\dot{}}{0}\right]$$
77	63	fmpttd	$$⊢\phi \to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}⟶{{\mathbb{N}}_0}^J$$
78		simpr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)$$
79		eqid	$$⊢\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)$$
80		reseq1	$$⊢x=u\to {x\upharpoonright }_J={u\upharpoonright }_J$$
81		simpllr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u\in \left\{y\in D|y\left(A\right)=0\right\}$$
82	81	resexd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {u\upharpoonright }_J\in \mathrm{V}$$
83	79 80 81 82	fvmptd3	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)={u\upharpoonright }_J$$
84		reseq1	$$⊢x=v\to {x\upharpoonright }_J={v\upharpoonright }_J$$
85		simplr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v\in \left\{y\in D|y\left(A\right)=0\right\}$$
86	85	resexd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {v\upharpoonright }_J\in \mathrm{V}$$
87	79 84 85 86	fvmptd3	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)={v\upharpoonright }_J$$
88	78 83 87	3eqtr3d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {u\upharpoonright }_J={v\upharpoonright }_J$$
89	6	a1i	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to J=I\setminus \left\{A\right\}$$
90	89	reseq2d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {u\upharpoonright }_J={u\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}$$
91	89	reseq2d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {v\upharpoonright }_J={v\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}$$
92	88 90 91	3eqtr3d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to {u\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}={v\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}$$
93		fveq1	$$⊢y=u\to y\left(A\right)=u\left(A\right)$$
94	93	eqeq1d	$$⊢y=u\to \left(y\left(A\right)=0\leftrightarrow u\left(A\right)=0\right)$$
95	94 81	elrabrd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u\left(A\right)=0$$
96		fveq1	$$⊢y=v\to y\left(A\right)=v\left(A\right)$$
97	96	eqeq1d	$$⊢y=v\to \left(y\left(A\right)=0\leftrightarrow v\left(A\right)=0\right)$$
98	97 85	elrabrd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v\left(A\right)=0$$
99	95 98	eqtr4d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u\left(A\right)=v\left(A\right)$$
100	99	opeq2d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to ⟨A,u\left(A\right)⟩=⟨A,v\left(A\right)⟩$$
101	100	sneqd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to \left\{⟨A,u\left(A\right)⟩\right\}=\left\{⟨A,v\left(A\right)⟩\right\}$$
102	92 101	uneq12d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to \left({u\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,u\left(A\right)⟩\right\}=\left({v\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,v\left(A\right)⟩\right\}$$
103	57	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to D\subseteq {{\mathbb{N}}_0}^I$$
104	54 81	sselid	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u\in D$$
105	103 104	sseldd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u\in \left({{\mathbb{N}}_0}^I\right)$$
106	105	elmaprd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u:I⟶{\mathbb{N}}_0$$
107	106	ffnd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to uFnI$$
108	8	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to A\in I$$
109		fnsnsplit	$$⊢\left(uFnI\wedge A\in I\right)\to u=\left({u\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,u\left(A\right)⟩\right\}$$
110	107 108 109	syl2anc	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u=\left({u\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,u\left(A\right)⟩\right\}$$
111	54 85	sselid	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v\in D$$
112	103 111	sseldd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v\in \left({{\mathbb{N}}_0}^I\right)$$
113	112	elmaprd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v:I⟶{\mathbb{N}}_0$$
114	113	ffnd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to vFnI$$
115		fnsnsplit	$$⊢\left(vFnI\wedge A\in I\right)\to v=\left({v\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,v\left(A\right)⟩\right\}$$
116	114 108 115	syl2anc	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to v=\left({v\upharpoonright }_{\left(I\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,v\left(A\right)⟩\right\}$$
117	102 110 116	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\right)\to u=v$$
118	117	ex	$$⊢\left(\left(\phi \wedge u\in \left\{y\in D|y\left(A\right)=0\right\}\right)\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\to \left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\to u=v\right)$$
119	118	anasss	$$⊢\left(\phi \wedge \left(u\in \left\{y\in D|y\left(A\right)=0\right\}\wedge v\in \left\{y\in D|y\left(A\right)=0\right\}\right)\right)\to \left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\to u=v\right)$$
120	119	ralrimivva	$$⊢\phi \to \forall u\in \left\{y\in D|y\left(A\right)=0\right\}\forall v\in \left\{y\in D|y\left(A\right)=0\right\}\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\to u=v\right)$$
121		dff13	$$⊢\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}\underset{1-1}{⟶}{{\mathbb{N}}_0}^J\leftrightarrow \left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}⟶{{\mathbb{N}}_0}^J\wedge \forall u\in \left\{y\in D|y\left(A\right)=0\right\}\forall v\in \left\{y\in D|y\left(A\right)=0\right\}\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(u\right)=\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\left(v\right)\to u=v\right)\right)$$
122	77 120 121	sylanbrc	$$⊢\phi \to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}\underset{1-1}{⟶}{{\mathbb{N}}_0}^J$$
123		df-f1	$$⊢\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}\underset{1-1}{⟶}{{\mathbb{N}}_0}^J\leftrightarrow \left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}⟶{{\mathbb{N}}_0}^J\wedge \mathrm{Fun}{\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\right)$$
124	123	simprbi	$$⊢\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right):\left\{y\in D|y\left(A\right)=0\right\}\underset{1-1}{⟶}{{\mathbb{N}}_0}^J\to \mathrm{Fun}{\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}$$
125	122 124	syl	$$⊢\phi \to \mathrm{Fun}{\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}$$
126	49 7 2 9	mplelsfi	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
127	126	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
128		imafi	$$⊢\left(\mathrm{Fun}{\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\wedge F\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)\to {\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\left[F\mathrm{supp}\underset{\dot{}}{0}\right]\in \mathrm{Fin}$$
129	125 127 128	syl2anc	$$⊢\phi \to {\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)}^{-1}\left[F\mathrm{supp}\underset{\dot{}}{0}\right]\in \mathrm{Fin}$$
130	76 129	eqeltrd	$$⊢\phi \to \left(F\circ \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼{x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
131	73 130	eqeltrrd	$$⊢\phi \to \left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
132		fconstmpt	$$⊢\left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)$$
133	132	oveq1i	$$⊢\left(\left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}=\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\mathrm{supp}\underset{\dot{}}{0}$$
134		fczsupp0	$$⊢\left(\left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)\times \left\{\underset{\dot{}}{0}\right\}\right)\mathrm{supp}\underset{\dot{}}{0}=\varnothing$$
135	133 134	eqtr3i	$$⊢\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\mathrm{supp}\underset{\dot{}}{0}=\varnothing$$
136		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
137	135 136	eqeltri	$$⊢\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
138	137	a1i	$$⊢\phi \to \left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
139	131 138	unfid	$$⊢\phi \to {supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left\{y\in D|y\left(A\right)=0\right\}⟼F\left({x\upharpoonright }_J\right)\right)\right)\cup {supp}_{\underset{\dot{}}{0}}\left(\left(x\in \left(D\setminus \left\{y\in D|y\left(A\right)=0\right\}\right)⟼\underset{\dot{}}{0}\right)\right)\in \mathrm{Fin}$$
140	48 139	eqeltrd	$$⊢\phi \to \left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
141	34 35 37 140	isfsuppd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in D⟼if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\right)\right)$$
142	20 141	eqbrtrd	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) with typecode |-
143		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
144	143 29 31 2 10	mplelbas	Could not format ( ( ( ( I extendVars R ) ` A ) ` F ) e. N <-> ( ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) ) : No typesetting found for |- ( ( ( ( I extendVars R ) ` A ) ` F ) e. N <-> ( ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) ) with typecode |-
145	33 142 144	sylanbrc	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N ) with typecode |-