Theorem mplvrpmga

Description: The action of permuting variables in a multivariate polynomial is a group action. (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$$
Assertion	mplvrpmga	$$⊢\phi \to A\in \left(S\mathrm{GrpAct}M\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	1	symggrp	$$⊢I\in V\to S\in \mathrm{Grp}$$
7	5 6	syl	$$⊢\phi \to S\in \mathrm{Grp}$$
8	3	fvexi	$$⊢M\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to M\in \mathrm{V}$$
10		fvexd	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to {\mathrm{Base}}_R\in \mathrm{V}$$
11		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
12	11	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
13	12	a1i	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
14		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16		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\}$$
17	16	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\}$$
18		xp2nd	$$⊢c\in \left(P\times M\right)\to 2^{nd}\left(c\right)\in M$$
19	18	ad2antlr	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 2^{nd}\left(c\right)\in M$$
20	14 15 3 17 19	mplelf	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 2^{nd}\left(c\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
21		breq1	$$⊢h=x\circ 1^{st}\left(c\right)\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(x\circ 1^{st}\left(c\right)\right)\right)\right)$$
22		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
23	22	a1i	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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	ad2antrr	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
25		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
26	25	a1i	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
27	26	sselda	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\in \left({{\mathbb{N}}_0}^I\right)$$
28	24 23 27	elmaprd	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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		xp1st	$$⊢c\in \left(P\times M\right)\to 1^{st}\left(c\right)\in P$$
30	29	ad2antlr	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1^{st}\left(c\right)\in P$$
31	1 2	symgbasf	$$⊢1^{st}\left(c\right)\in P\to 1^{st}\left(c\right):I⟶I$$
32	30 31	syl	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1^{st}\left(c\right):I⟶I$$
33	28 32	fcod	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(x\circ 1^{st}\left(c\right)\right):I⟶{\mathbb{N}}_0$$
34	23 24 33	elmapdd	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ 1^{st}\left(c\right)\in \left({{\mathbb{N}}_0}^I\right)$$
35		simpr	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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\}$$
36		breq1	$$⊢h=x\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(x\right)\right)$$
37	36	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)$$
38	35 37	sylib	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(x\in \left({{\mathbb{N}}_0}^I\right)\wedge {finSupp}_0\left(x\right)\right)$$
39	38	simprd	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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)$$
40	1 2	symgbasf1o	$$⊢1^{st}\left(c\right)\in P\to 1^{st}\left(c\right):I\underset{1-1\; onto}{⟶}I$$
41		f1of1	$$⊢1^{st}\left(c\right):I\underset{1-1\; onto}{⟶}I\to 1^{st}\left(c\right):I\underset{1-1}{⟶}I$$
42	30 40 41	3syl	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1^{st}\left(c\right):I\underset{1-1}{⟶}I$$
43		0nn0	$$⊢0\in {\mathbb{N}}_0$$
44	43	a1i	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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$$
45	39 42 44 35	fsuppco	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\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 1^{st}\left(c\right)\right)\right)$$
46	21 34 45	elrabd	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ 1^{st}\left(c\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
47	20 46	ffvelcdmd	$$⊢\left(\left(\phi \wedge c\in \left(P\times M\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\in {\mathrm{Base}}_R$$
48	47	fmpttd	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
49	10 13 48	elmapdd	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\in \left({{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}\right)$$
50		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
51		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
52	50 15 17 51 5	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}$$
53	52	adantr	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}$$
54	49 53	eleqtrrd	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
55		coeq1	$$⊢x=y\to x\circ 1^{st}\left(c\right)=y\circ 1^{st}\left(c\right)$$
56	55	fveq2d	$$⊢x=y\to 2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)=2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)$$
57	56	cbvmptv	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)\right)$$
58		fveq1	$$⊢g=2^{nd}\left(c\right)\to g\left(y\circ q\right)=2^{nd}\left(c\right)\left(y\circ q\right)$$
59	58	mpteq2dv	$$⊢g=2^{nd}\left(c\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ q\right)\right)$$
60	59	breq1d	$$⊢g=2^{nd}\left(c\right)\to \left({finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\leftrightarrow {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ q\right)\right)\right)\right)$$
61		coeq2	$$⊢q=1^{st}\left(c\right)\to y\circ q=y\circ 1^{st}\left(c\right)$$
62	61	fveq2d	$$⊢q=1^{st}\left(c\right)\to 2^{nd}\left(c\right)\left(y\circ q\right)=2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)$$
63	62	mpteq2dv	$$⊢q=1^{st}\left(c\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ q\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)\right)$$
64	63	breq1d	$$⊢q=1^{st}\left(c\right)\to \left({finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ q\right)\right)\right)\leftrightarrow {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)\right)\right)\right)$$
65	4	a1i	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\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)$$
66		simpr	$$⊢\left(d=q\wedge f=g\right)\to f=g$$
67		coeq2	$$⊢d=q\to x\circ d=x\circ q$$
68	67	adantr	$$⊢\left(d=q\wedge f=g\right)\to x\circ d=x\circ q$$
69	66 68	fveq12d	$$⊢\left(d=q\wedge f=g\right)\to f\left(x\circ d\right)=g\left(x\circ q\right)$$
70	69	mpteq2dv	$$⊢\left(d=q\wedge f=g\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\}⟼g\left(x\circ q\right)\right)$$
71	70	adantl	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\wedge \left(d=q\wedge f=g\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\}⟼g\left(x\circ q\right)\right)$$
72		simpr	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to q\in P$$
73		simplr	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to g\in M$$
74	12	mptex	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ q\right)\right)\in \mathrm{V}$$
75	74	a1i	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ q\right)\right)\in \mathrm{V}$$
76	65 71 72 73 75	ovmpod	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to qAg=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ q\right)\right)$$
77		coeq1	$$⊢x=y\to x\circ q=y\circ q$$
78	77	fveq2d	$$⊢x=y\to g\left(x\circ q\right)=g\left(y\circ q\right)$$
79	78	cbvmptv	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ q\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
80	76 79	eqtrdi	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to qAg=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
81	5	ad2antrr	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to I\in V$$
82		eqid	$$⊢0_R=0_R$$
83	1 2 3 4 81 82 73 72	mplvrpmfgalem	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to {finSupp}_{0_R}\left(\left(qAg\right)\right)$$
84	80 83	eqbrtrrd	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge q\in P\right)\to {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
85	84	anasss	$$⊢\left(\phi \wedge \left(g\in M\wedge q\in P\right)\right)\to {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
86	85	ralrimivva	$$⊢\phi \to \forall g\in M\forall q\in P{finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
87	86	adantr	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \forall g\in M\forall q\in P{finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
88	18	adantl	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to 2^{nd}\left(c\right)\in M$$
89	29	adantl	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to 1^{st}\left(c\right)\in P$$
90	60 64 87 88 89	rspc2dv	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(y\circ 1^{st}\left(c\right)\right)\right)\right)$$
91	57 90	eqbrtrid	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to {finSupp}_{0_R}\left(\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\right)$$
92	14 50 51 82 3	mplelbas	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\in M\leftrightarrow \left(\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{0_R}\left(\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\right)\right)$$
93	54 91 92	sylanbrc	$$⊢\left(\phi \wedge c\in \left(P\times M\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\in M$$
94		vex	$$⊢d\in \mathrm{V}$$
95		vex	$$⊢f\in \mathrm{V}$$
96	94 95	op2ndd	$$⊢c=⟨d,f⟩\to 2^{nd}\left(c\right)=f$$
97	94 95	op1std	$$⊢c=⟨d,f⟩\to 1^{st}\left(c\right)=d$$
98	97	coeq2d	$$⊢c=⟨d,f⟩\to x\circ 1^{st}\left(c\right)=x\circ d$$
99	96 98	fveq12d	$$⊢c=⟨d,f⟩\to 2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)=f\left(x\circ d\right)$$
100	99	mpteq2dv	$$⊢c=⟨d,f⟩\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)=\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)$$
101	100	mpompt	$$⊢\left(c\in \left(P\times M\right)⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\right)=\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)$$
102	4 101	eqtr4i	$$⊢A=\left(c\in \left(P\times M\right)⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼2^{nd}\left(c\right)\left(x\circ 1^{st}\left(c\right)\right)\right)\right)$$
103	93 102	fmptd	$$⊢\phi \to A:P\times M⟶M$$
104	1	symgid	$$⊢I\in V\to {\mathrm{I}\upharpoonright }_I=0_S$$
105	5 104	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_I=0_S$$
106	105	adantr	$$⊢\left(\phi \wedge g\in M\right)\to {\mathrm{I}\upharpoonright }_I=0_S$$
107	106	oveq1d	$$⊢\left(\phi \wedge g\in M\right)\to \left({\mathrm{I}\upharpoonright }_I\right)Ag=0_{S}Ag$$
108	4	a1i	$$⊢\left(\phi \wedge g\in M\right)\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)$$
109	5	ad2antrr	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
110	22	a1i	$$⊢\left(\left(\phi \wedge g\in M\right)\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}$$
111	25	a1i	$$⊢\left(\phi \wedge g\in M\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
112	111	sselda	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\in \left({{\mathbb{N}}_0}^I\right)$$
113	109 110 112	elmaprd	$$⊢\left(\left(\phi \wedge g\in M\right)\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$$
114		fcoi1	$$⊢x:I⟶{\mathbb{N}}_0\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
115	113 114	syl	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
116	115	fveq2d	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)=g\left(x\right)$$
117	116	mpteq2dva	$$⊢\left(\phi \wedge g\in M\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\right)\right)$$
118	117	adantr	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge \left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\right)\right)$$
119		simpr	$$⊢\left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\right)\to f=g$$
120		coeq2	$$⊢d={\mathrm{I}\upharpoonright }_I\to x\circ d=x\circ \left({\mathrm{I}\upharpoonright }_I\right)$$
121	120	adantr	$$⊢\left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\right)\to x\circ d=x\circ \left({\mathrm{I}\upharpoonright }_I\right)$$
122	119 121	fveq12d	$$⊢\left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\right)\to f\left(x\circ d\right)=g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)$$
123	122	mpteq2dv	$$⊢\left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\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\}⟼g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)\right)$$
124	123	adantl	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge \left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\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\}⟼g\left(x\circ \left({\mathrm{I}\upharpoonright }_I\right)\right)\right)$$
125	14 50 51 82 3	mplelbas	$$⊢g\in M\leftrightarrow \left(g\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{0_R}\left(g\right)\right)$$
126	125	simplbi	$$⊢g\in M\to g\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
127	50 15 17 51 126	psrelbas	$$⊢g\in M\to g:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
128	127	ad3antlr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge d={\mathrm{I}\upharpoonright }_I\right)\wedge f=g\right)\to g:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
129	128	feqmptd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge d={\mathrm{I}\upharpoonright }_I\right)\wedge f=g\right)\to g=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\right)\right)$$
130	129	anasss	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge \left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\right)\right)\to g=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\right)\right)$$
131	118 124 130	3eqtr4d	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge \left(d={\mathrm{I}\upharpoonright }_I\wedge f=g\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)=g$$
132		eqid	$$⊢0_S=0_S$$
133	2 132	grpidcl	$$⊢S\in \mathrm{Grp}\to 0_S\in P$$
134	5 6 133	3syl	$$⊢\phi \to 0_S\in P$$
135	105 134	eqeltrd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_I\in P$$
136	135	adantr	$$⊢\left(\phi \wedge g\in M\right)\to {\mathrm{I}\upharpoonright }_I\in P$$
137		simpr	$$⊢\left(\phi \wedge g\in M\right)\to g\in M$$
138	108 131 136 137 137	ovmpod	$$⊢\left(\phi \wedge g\in M\right)\to \left({\mathrm{I}\upharpoonright }_I\right)Ag=g$$
139	107 138	eqtr3d	$$⊢\left(\phi \wedge g\in M\right)\to 0_{S}Ag=g$$
140		eqid	$$⊢{+}_S={+}_S$$
141	1 2 140	symgov	$$⊢\left(p\in P\wedge q\in P\right)\to p{+}_{S}q=p\circ q$$
142	141	adantll	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to p{+}_{S}q=p\circ q$$
143	142	oveq1d	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(p{+}_{S}q\right)Ag=\left(p\circ q\right)Ag$$
144		coass	$$⊢\left(x\circ p\right)\circ q=x\circ \left(p\circ q\right)$$
145	144	a1i	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(x\circ p\right)\circ q=x\circ \left(p\circ q\right)$$
146	145	fveq2d	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g\left(\left(x\circ p\right)\circ q\right)=g\left(x\circ \left(p\circ q\right)\right)$$
147	146	mpteq2dva	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ \left(p\circ q\right)\right)\right)$$
148	80	adantlr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to qAg=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
149	148	oveq2d	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to pA\left(qAg\right)=pA\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
150	4	a1i	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\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)$$
151		simpllr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to d=p$$
152	151	coeq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ d=x\circ p$$
153	152	fveq2d	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to f\left(x\circ d\right)=f\left(x\circ p\right)$$
154		simplr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
155		simpr	$$⊢\left(\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y=x\circ p\right)\to y=x\circ p$$
156	155	coeq1d	$$⊢\left(\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y=x\circ p\right)\to y\circ q=\left(x\circ p\right)\circ q$$
157	156	fveq2d	$$⊢\left(\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y=x\circ p\right)\to g\left(y\circ q\right)=g\left(\left(x\circ p\right)\circ q\right)$$
158		breq1	$$⊢h=x\circ p\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(x\circ p\right)\right)\right)$$
159	22	a1i	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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}$$
160	5	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to I\in V$$
161	160	ad3antrrr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
162	25	a1i	$$⊢\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
163	162	sselda	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\in \left({{\mathbb{N}}_0}^I\right)$$
164	161 159 163	elmaprd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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$$
165	1 2	symgbasf	$$⊢p\in P\to p:I⟶I$$
166	165	ad5antlr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p:I⟶I$$
167	164 166	fcod	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(x\circ p\right):I⟶{\mathbb{N}}_0$$
168	159 161 167	elmapdd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ p\in \left({{\mathbb{N}}_0}^I\right)$$
169	37	simprbi	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to {finSupp}_0\left(x\right)$$
170	169	adantl	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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)$$
171	1 2	symgbasf1o	$$⊢p\in P\to p:I\underset{1-1\; onto}{⟶}I$$
172		f1of1	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p:I\underset{1-1}{⟶}I$$
173	171 172	syl	$$⊢p\in P\to p:I\underset{1-1}{⟶}I$$
174	173	ad5antlr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to p:I\underset{1-1}{⟶}I$$
175	43	a1i	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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$$
176		simpr	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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\}$$
177	170 174 175 176	fsuppco	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\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 p\right)\right)$$
178	158 168 177	elrabd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
179		fvexd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g\left(\left(x\circ p\right)\circ q\right)\in \mathrm{V}$$
180		nfv	$$⊢Ⅎy\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)$$
181		nfmpt1	$$⊢\underset{\_}{Ⅎ}y\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
182	181	nfeq2	$$⊢Ⅎyf=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)$$
183	180 182	nfan	$$⊢Ⅎy\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
184		nfv	$$⊢Ⅎyx\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
185	183 184	nfan	$$⊢Ⅎy\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)$$
186		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(x\circ p\right)$$
187		nfcv	$$⊢\underset{\_}{Ⅎ}yg\left(\left(x\circ p\right)\circ q\right)$$
188	154 157 178 179 185 186 187	fvmptdf	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to f\left(x\circ p\right)=g\left(\left(x\circ p\right)\circ q\right)$$
189	153 188	eqtrd	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to f\left(x\circ d\right)=g\left(\left(x\circ p\right)\circ q\right)$$
190	189	mpteq2dva	$$⊢\left(\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge d=p\right)\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\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\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)$$
191	190	anasss	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge \left(d=p\wedge f=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\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\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)$$
192		simplr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to p\in P$$
193		fvexd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to {\mathrm{Base}}_R\in \mathrm{V}$$
194	12	a1i	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
195	137	ad3antrrr	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g\in M$$
196	14 15 3 17 195	mplelf	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
197		breq1	$$⊢h=y\circ q\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(y\circ q\right)\right)\right)$$
198	22	a1i	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
199	160	adantr	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to I\in V$$
200	25	a1i	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
201	200	sselda	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to y\in \left({{\mathbb{N}}_0}^I\right)$$
202	199 198 201	elmaprd	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to y:I⟶{\mathbb{N}}_0$$
203	1 2	symgbasf	$$⊢q\in P\to q:I⟶I$$
204	203	ad2antlr	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to q:I⟶I$$
205	202 204	fcod	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(y\circ q\right):I⟶{\mathbb{N}}_0$$
206	198 199 205	elmapdd	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to y\circ q\in \left({{\mathbb{N}}_0}^I\right)$$
207		breq1	$$⊢h=y\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(y\right)\right)$$
208	207	elrab	$$⊢y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\leftrightarrow \left(y\in \left({{\mathbb{N}}_0}^I\right)\wedge {finSupp}_0\left(y\right)\right)$$
209	208	simprbi	$$⊢y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to {finSupp}_0\left(y\right)$$
210	209	adantl	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(y\right)$$
211	1 2	symgbasf1o	$$⊢q\in P\to q:I\underset{1-1\; onto}{⟶}I$$
212	211	ad2antlr	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to q:I\underset{1-1\; onto}{⟶}I$$
213		f1of1	$$⊢q:I\underset{1-1\; onto}{⟶}I\to q:I\underset{1-1}{⟶}I$$
214	212 213	syl	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to q:I\underset{1-1}{⟶}I$$
215	43	a1i	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0\in {\mathbb{N}}_0$$
216		simpr	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
217	210 214 215 216	fsuppco	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_0\left(\left(y\circ q\right)\right)$$
218	197 206 217	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to y\circ q\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
219	196 218	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to g\left(y\circ q\right)\in {\mathrm{Base}}_R$$
220	219	fmpttd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
221	193 194 220	elmapdd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\in \left({{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}\right)$$
222	52	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}$$
223	221 222	eleqtrrd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
224	84	adantlr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)$$
225	14 50 51 82 3	mplelbas	$$⊢\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\in M\leftrightarrow \left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{0_R}\left(\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\right)\right)$$
226	223 224 225	sylanbrc	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)\in M$$
227	194	mptexd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)\in \mathrm{V}$$
228	150 191 192 226 227	ovmpod	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to pA\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(y\circ q\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)$$
229	149 228	eqtrd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to pA\left(qAg\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(\left(x\circ p\right)\circ q\right)\right)$$
230		simpr	$$⊢\left(d=p\circ q\wedge f=g\right)\to f=g$$
231		coeq2	$$⊢d=p\circ q\to x\circ d=x\circ \left(p\circ q\right)$$
232	231	adantr	$$⊢\left(d=p\circ q\wedge f=g\right)\to x\circ d=x\circ \left(p\circ q\right)$$
233	230 232	fveq12d	$$⊢\left(d=p\circ q\wedge f=g\right)\to f\left(x\circ d\right)=g\left(x\circ \left(p\circ q\right)\right)$$
234	233	mpteq2dv	$$⊢\left(d=p\circ q\wedge f=g\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\}⟼g\left(x\circ \left(p\circ q\right)\right)\right)$$
235	234	adantl	$$⊢\left(\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\wedge \left(d=p\circ q\wedge f=g\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\}⟼g\left(x\circ \left(p\circ q\right)\right)\right)$$
236	160 6	syl	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to S\in \mathrm{Grp}$$
237		simpr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to q\in P$$
238	2 140 236 192 237	grpcld	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to p{+}_{S}q\in P$$
239	142 238	eqeltrrd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to p\circ q\in P$$
240		simpllr	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to g\in M$$
241	194	mptexd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ \left(p\circ q\right)\right)\right)\in \mathrm{V}$$
242	150 235 239 240 241	ovmpod	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(p\circ q\right)Ag=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ \left(p\circ q\right)\right)\right)$$
243	147 229 242	3eqtr4rd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(p\circ q\right)Ag=pA\left(qAg\right)$$
244	143 243	eqtrd	$$⊢\left(\left(\left(\phi \wedge g\in M\right)\wedge p\in P\right)\wedge q\in P\right)\to \left(p{+}_{S}q\right)Ag=pA\left(qAg\right)$$
245	244	anasss	$$⊢\left(\left(\phi \wedge g\in M\right)\wedge \left(p\in P\wedge q\in P\right)\right)\to \left(p{+}_{S}q\right)Ag=pA\left(qAg\right)$$
246	245	ralrimivva	$$⊢\left(\phi \wedge g\in M\right)\to \forall p\in P\forall q\in P\left(p{+}_{S}q\right)Ag=pA\left(qAg\right)$$
247	139 246	jca	$$⊢\left(\phi \wedge g\in M\right)\to \left(0_{S}Ag=g\wedge \forall p\in P\forall q\in P\left(p{+}_{S}q\right)Ag=pA\left(qAg\right)\right)$$
248	247	ralrimiva	$$⊢\phi \to \forall g\in M\left(0_{S}Ag=g\wedge \forall p\in P\forall q\in P\left(p{+}_{S}q\right)Ag=pA\left(qAg\right)\right)$$
249	2 140 132	isga	$$⊢A\in \left(S\mathrm{GrpAct}M\right)\leftrightarrow \left(\left(S\in \mathrm{Grp}\wedge M\in \mathrm{V}\right)\wedge \left(A:P\times M⟶M\wedge \forall g\in M\left(0_{S}Ag=g\wedge \forall p\in P\forall q\in P\left(p{+}_{S}q\right)Ag=pA\left(qAg\right)\right)\right)\right)$$
250	7 9 103 248 249	syl22anbrc	$$⊢\phi \to A\in \left(S\mathrm{GrpAct}M\right)$$