Theorem mplvrpmfgalem

Description: Permuting variables in a multivariate polynomial conserves finite support. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	mplvrpmga.1	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
	mplvrpmga.2	$$⊢P={\mathrm{Base}}_S$$
	mplvrpmga.3	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
	mplvrpmga.4	$$⊢A=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
	mplvrpmga.5	$$⊢\phi \to I\in V$$
	mplvrpmfgalem.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplvrpmfgalem.f	$$⊢\phi \to F\in M$$
	mplvrpmfgalem.q	$$⊢\phi \to Q\in P$$
Assertion	mplvrpmfgalem	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(QAF\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplvrpmga.1	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
2		mplvrpmga.2	$$⊢P={\mathrm{Base}}_S$$
3		mplvrpmga.3	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
4		mplvrpmga.4	$$⊢A=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
5		mplvrpmga.5	$$⊢\phi \to I\in V$$
6		mplvrpmfgalem.z	$$⊢\underset{\dot{}}{0}=0_R$$
7		mplvrpmfgalem.f	$$⊢\phi \to F\in M$$
8		mplvrpmfgalem.q	$$⊢\phi \to Q\in P$$
9	4	a1i	$$⊢\phi \to A=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
10		simpr	$$⊢\left(d=Q\wedge f=F\right)\to f=F$$
11		coeq2	$$⊢d=Q\to x\circ d=x\circ Q$$
12	11	adantr	$$⊢\left(d=Q\wedge f=F\right)\to x\circ d=x\circ Q$$
13	10 12	fveq12d	$$⊢\left(d=Q\wedge f=F\right)\to f\left(x\circ d\right)=F\left(x\circ Q\right)$$
14	13	mpteq2dv	$$⊢\left(d=Q\wedge f=F\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)$$
15	14	adantl	$$⊢\left(\phi \wedge \left(d=Q\wedge f=F\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)$$
16		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
19	18	mptexd	$$⊢\phi \to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)\in \mathrm{V}$$
20	9 15 8 7 19	ovmpod	$$⊢\phi \to QAF=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)$$
21		breq1	$$⊢h=x\circ Q\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(x\circ Q\right)\right)\right)$$
22		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
23	22	a1i	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
24	5	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
25		eqid	$$⊢\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\}$$
26	25	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
27	26	psrbagf	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to x:I⟶{\mathbb{N}}_0$$
28	27	adantl	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x:I⟶{\mathbb{N}}_0$$
29	1 2	symgbasf1o	$$⊢Q\in P\to Q:I\underset{1-1\; onto}{⟶}I$$
30	8 29	syl	$$⊢\phi \to Q:I\underset{1-1\; onto}{⟶}I$$
31		f1of	$$⊢Q:I\underset{1-1\; onto}{⟶}I\to Q:I⟶I$$
32	30 31	syl	$$⊢\phi \to Q:I⟶I$$
33	32	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to Q:I⟶I$$
34	28 33	fcod	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(x\circ Q\right):I⟶{\mathbb{N}}_0$$
35	23 24 34	elmapdd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ Q\in \left({{\mathbb{N}}_0}^I\right)$$
36	26	psrbagfsupp	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to {finSupp}_0\left(x\right)$$
37	36	adantl	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(x\right)$$
38		f1of1	$$⊢Q:I\underset{1-1\; onto}{⟶}I\to Q:I\underset{1-1}{⟶}I$$
39	30 38	syl	$$⊢\phi \to Q:I\underset{1-1}{⟶}I$$
40	39	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to Q:I\underset{1-1}{⟶}I$$
41		0nn0	$$⊢0\in {\mathbb{N}}_0$$
42	41	a1i	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0\in {\mathbb{N}}_0$$
43		simpr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
44	37 40 42 43	fsuppco	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(\left(x\circ Q\right)\right)$$
45	21 35 44	elrabd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ Q\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
46		eqidd	$$⊢\phi \to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right)$$
47		eqidd	$$⊢\phi \to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)$$
48		fveq2	$$⊢y=x\circ Q\to F\left(y\right)=F\left(x\circ Q\right)$$
49	45 46 47 48	fmptco	$$⊢\phi \to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)\circ \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)$$
50		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
51		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
52	50 51 3 26 7	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
53	52	feqmptd	$$⊢\phi \to F=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)$$
54	50 3 6 7	mplelsfi	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
55	53 54	breq1dd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)\right)$$
56	22	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
57	41	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
58		breq1	$$⊢h=g\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(g\right)\right)$$
59	58	cbvrabv	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{g\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(g\right)\right\}$$
60	30 5 5 56 57 25 59	fcobijfs2	$$⊢\phi \to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\underset{1-1\; onto}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
61		f1of1	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\underset{1-1\; onto}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\underset{1-1}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
62	60 61	syl	$$⊢\phi \to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\underset{1-1}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
63	6	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
64	63	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
65	18	mptexd	$$⊢\phi \to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)\in \mathrm{V}$$
66	55 62 64 65	fsuppco	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(y\right)\right)\circ \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼x\circ Q\right)\right)\right)$$
67	49 66	breq1dd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼F\left(x\circ Q\right)\right)\right)$$
68	20 67	eqbrtrd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(QAF\right)\right)$$