Theorem mplvrpmlem

Description: Lemma for mplvrpmga and others. (Contributed by Thierry Arnoux, 11-Jan-2026)

	Ref	Expression
Hypotheses	mplvrpmlem.s	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
	mplvrpmlem.p	$$⊢P={\mathrm{Base}}_S$$
	mplvrpmlem.i	$$⊢\phi \to I\in V$$
	mplvrpmlem.d	$$⊢\phi \to D\in P$$
	mplvrpmlem.1	$$⊢\phi \to X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
Assertion	mplvrpmlem	$$⊢\phi \to X\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mplvrpmlem.s	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
2		mplvrpmlem.p	$$⊢P={\mathrm{Base}}_S$$
3		mplvrpmlem.i	$$⊢\phi \to I\in V$$
4		mplvrpmlem.d	$$⊢\phi \to D\in P$$
5		mplvrpmlem.1	$$⊢\phi \to X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
6		breq1	$$⊢h=X\circ D\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(X\circ D\right)\right)\right)$$
7		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
8	7	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
9		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
10	9 5	sselid	$$⊢\phi \to X\in \left({{\mathbb{N}}_0}^I\right)$$
11	3 8 10	elmaprd	$$⊢\phi \to X:I⟶{\mathbb{N}}_0$$
12	1 2	symgbasf1o	$$⊢D\in P\to D:I\underset{1-1\; onto}{⟶}I$$
13	4 12	syl	$$⊢\phi \to D:I\underset{1-1\; onto}{⟶}I$$
14		f1of	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D:I⟶I$$
15	13 14	syl	$$⊢\phi \to D:I⟶I$$
16	11 15	fcod	$$⊢\phi \to \left(X\circ D\right):I⟶{\mathbb{N}}_0$$
17	8 3 16	elmapdd	$$⊢\phi \to X\circ D\in \left({{\mathbb{N}}_0}^I\right)$$
18		breq1	$$⊢h=X\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(X\right)\right)$$
19	18	elrab	$$⊢X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\leftrightarrow \left(X\in \left({{\mathbb{N}}_0}^I\right)\wedge {finSupp}_0\left(X\right)\right)$$
20	19	simprbi	$$⊢X\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to {finSupp}_0\left(X\right)$$
21	5 20	syl	$$⊢\phi \to {finSupp}_0\left(X\right)$$
22		f1of1	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D:I\underset{1-1}{⟶}I$$
23	13 22	syl	$$⊢\phi \to D:I\underset{1-1}{⟶}I$$
24		0nn0	$$⊢0\in {\mathbb{N}}_0$$
25	24	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
26	21 23 25 5	fsuppco	$$⊢\phi \to {finSupp}_0\left(\left(X\circ D\right)\right)$$
27	6 17 26	elrabd	$$⊢\phi \to X\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$