Theorem mplvrpmrhm

Description: The action of permuting variables in a multivariate polynomial is a ring homomorphism. (Contributed by Thierry Arnoux, 15-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$$
	mplvrpmmhm.f	$$⊢F=\left(f\in M⟼DAf\right)$$
	mplvrpmmhm.w	$$⊢W=I\mathrm{mPoly}R$$
	mplvrpmmhm.1	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplvrpmmhm.2	$$⊢\phi \to D\in P$$
Assertion	mplvrpmrhm	$$⊢\phi \to F\in \left(W\mathrm{RingHom}W\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		mplvrpmmhm.f	$$⊢F=\left(f\in M⟼DAf\right)$$
7		mplvrpmmhm.w	$$⊢W=I\mathrm{mPoly}R$$
8		mplvrpmmhm.1	$$⊢\phi \to R\in \mathrm{Ring}$$
9		mplvrpmmhm.2	$$⊢\phi \to D\in P$$
10	7	fveq2i	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
11	3 10	eqtr4i	$$⊢M={\mathrm{Base}}_W$$
12		eqid	$$⊢1_W=1_W$$
13		eqid	$$⊢{\cdot }_W={\cdot }_W$$
14	7 5 8	mplringd	$$⊢\phi \to W\in \mathrm{Ring}$$
15		oveq2	$$⊢f=1_W\to DAf=DA{1}_W$$
16	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)$$
17		simpr	$$⊢\left(d=D\wedge f=1_W\right)\to f=1_W$$
18		simpl	$$⊢\left(d=D\wedge f=1_W\right)\to d=D$$
19	18	coeq2d	$$⊢\left(d=D\wedge f=1_W\right)\to x\circ d=x\circ D$$
20	17 19	fveq12d	$$⊢\left(d=D\wedge f=1_W\right)\to f\left(x\circ d\right)=1_W\left(x\circ D\right)$$
21	20	ad2antlr	$$⊢\left(\left(\phi \wedge \left(d=D\wedge f=1_W\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)=1_W\left(x\circ D\right)$$
22		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\}$$
23	22	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\}$$
24		eqid	$$⊢0_R=0_R$$
25		eqid	$$⊢1_R=1_R$$
26	7 23 24 25 12 5 8	mpl1	$$⊢\phi \to 1_W=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(y=I\times \left\{0\right\},1_R,0_R\right)\right)$$
27	26	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1_W=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(y=I\times \left\{0\right\},1_R,0_R\right)\right)$$
28		eqeq1	$$⊢y=x\circ D\to \left(y=I\times \left\{0\right\}\leftrightarrow x\circ D=I\times \left\{0\right\}\right)$$
29	9	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to D\in P$$
30	1 2	symgbasf1o	$$⊢D\in P\to D:I\underset{1-1\; onto}{⟶}I$$
31		f1ococnv2	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D\circ D^{-1}={\mathrm{I}\upharpoonright }_I$$
32	29 30 31	3syl	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to D\circ D^{-1}={\mathrm{I}\upharpoonright }_I$$
33	32	adantr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to D\circ D^{-1}={\mathrm{I}\upharpoonright }_I$$
34	33	coeq2d	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to x\circ \left(D\circ D^{-1}\right)=x\circ \left({\mathrm{I}\upharpoonright }_I\right)$$
35		simpr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to x\circ D=I\times \left\{0\right\}$$
36	35	coeq1d	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to \left(x\circ D\right)\circ D^{-1}=\left(I\times \left\{0\right\}\right)\circ D^{-1}$$
37		coass	$$⊢\left(x\circ D\right)\circ D^{-1}=x\circ \left(D\circ D^{-1}\right)$$
38	37	a1i	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to \left(x\circ D\right)\circ D^{-1}=x\circ \left(D\circ D^{-1}\right)$$
39	9 30	syl	$$⊢\phi \to D:I\underset{1-1\; onto}{⟶}I$$
40		f1ocnv	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D^{-1}:I\underset{1-1\; onto}{⟶}I$$
41		f1of	$$⊢D^{-1}:I\underset{1-1\; onto}{⟶}I\to D^{-1}:I⟶I$$
42	39 40 41	3syl	$$⊢\phi \to D^{-1}:I⟶I$$
43		0nn0	$$⊢0\in {\mathbb{N}}_0$$
44	43	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
45	42 44	constcof	$$⊢\phi \to \left(I\times \left\{0\right\}\right)\circ D^{-1}=I\times \left\{0\right\}$$
46	45	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to \left(I\times \left\{0\right\}\right)\circ D^{-1}=I\times \left\{0\right\}$$
47	36 38 46	3eqtr3d	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to x\circ \left(D\circ D^{-1}\right)=I\times \left\{0\right\}$$
48	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$$
49		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
50	49	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}$$
51		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
52		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\}$$
53	51 52	sselid	$$⊢\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({{\mathbb{N}}_0}^I\right)$$
54	48 50 53	elmaprd	$$⊢\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$$
55		fcoi1	$$⊢x:I⟶{\mathbb{N}}_0\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
56	54 55	syl	$$⊢\left(\phi \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$$
57	56	adantr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
58	34 47 57	3eqtr3rd	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x\circ D=I\times \left\{0\right\}\right)\to x=I\times \left\{0\right\}$$
59		simpr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x=I\times \left\{0\right\}\right)\to x=I\times \left\{0\right\}$$
60	59	coeq1d	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x=I\times \left\{0\right\}\right)\to x\circ D=\left(I\times \left\{0\right\}\right)\circ D$$
61		f1of	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D:I⟶I$$
62	9 30 61	3syl	$$⊢\phi \to D:I⟶I$$
63	62 44	constcof	$$⊢\phi \to \left(I\times \left\{0\right\}\right)\circ D=I\times \left\{0\right\}$$
64	63	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x=I\times \left\{0\right\}\right)\to \left(I\times \left\{0\right\}\right)\circ D=I\times \left\{0\right\}$$
65	60 64	eqtrd	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge x=I\times \left\{0\right\}\right)\to x\circ D=I\times \left\{0\right\}$$
66	58 65	impbida	$$⊢\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 D=I\times \left\{0\right\}\leftrightarrow x=I\times \left\{0\right\}\right)$$
67	28 66	sylan9bbr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y=x\circ D\right)\to \left(y=I\times \left\{0\right\}\leftrightarrow x=I\times \left\{0\right\}\right)$$
68	67	ifbid	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y=x\circ D\right)\to if\left(y=I\times \left\{0\right\},1_R,0_R\right)=if\left(x=I\times \left\{0\right\},1_R,0_R\right)$$
69	1 2 48 29 52	mplvrpmlem	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to x\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
70		fvexd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1_R\in \mathrm{V}$$
71		fvexd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0_R\in \mathrm{V}$$
72	70 71	ifcld	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to if\left(x=I\times \left\{0\right\},1_R,0_R\right)\in \mathrm{V}$$
73	27 68 69 72	fvmptd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1_W\left(x\circ D\right)=if\left(x=I\times \left\{0\right\},1_R,0_R\right)$$
74	73	adantlr	$$⊢\left(\left(\phi \wedge \left(d=D\wedge f=1_W\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1_W\left(x\circ D\right)=if\left(x=I\times \left\{0\right\},1_R,0_R\right)$$
75	21 74	eqtrd	$$⊢\left(\left(\phi \wedge \left(d=D\wedge f=1_W\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)=if\left(x=I\times \left\{0\right\},1_R,0_R\right)$$
76	75	mpteq2dva	$$⊢\left(\phi \wedge \left(d=D\wedge f=1_W\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\}⟼if\left(x=I\times \left\{0\right\},1_R,0_R\right)\right)$$
77	11 12 14	ringidcld	$$⊢\phi \to 1_W\in M$$
78		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
79	78	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
80	79	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
81	80	mptexd	$$⊢\phi \to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x=I\times \left\{0\right\},1_R,0_R\right)\right)\in \mathrm{V}$$
82	16 76 9 77 81	ovmpod	$$⊢\phi \to DA{1}_W=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x=I\times \left\{0\right\},1_R,0_R\right)\right)$$
83		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
84		eqid	$$⊢1_{\left(I\mathrm{mPwSer}R\right)}=1_{\left(I\mathrm{mPwSer}R\right)}$$
85	83 5 8 23 24 25 84	psr1	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(x=I\times \left\{0\right\},1_R,0_R\right)\right)$$
86	83 7 11 5 8	mplsubrg	$$⊢\phi \to M\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
87	7 83 11	mplval2	$$⊢W=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}M$$
88	87 84	subrg1	$$⊢M\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)\to 1_{\left(I\mathrm{mPwSer}R\right)}=1_W$$
89	86 88	syl	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}=1_W$$
90	82 85 89	3eqtr2d	$$⊢\phi \to DA{1}_W=1_W$$
91	15 90	sylan9eqr	$$⊢\left(\phi \wedge f=1_W\right)\to DAf=1_W$$
92	6 91 77 77	fvmptd2	$$⊢\phi \to F\left(1_W\right)=1_W$$
93		nfcv	$$⊢\underset{\_}{Ⅎ}v\left(i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)\right)$$
94		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
95		fveq2	$$⊢v=y\circ D\to i\left(v\right)=i\left(y\circ D\right)$$
96		oveq2	$$⊢v=y\circ D\to \left(x\circ D\right){-}_{f}v=\left(x\circ D\right){-}_f\left(y\circ D\right)$$
97	96	fveq2d	$$⊢v=y\circ D\to j\left(\left(x\circ D\right){-}_{f}v\right)=j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
98	95 97	oveq12d	$$⊢v=y\circ D\to i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)=i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
99	8	ringcmnd	$$⊢\phi \to R\in \mathrm{CMnd}$$
100	99	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to R\in \mathrm{CMnd}$$
101	79	rabex	$$⊢\left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\in \mathrm{V}$$
102	101	a1i	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\in \mathrm{V}$$
103		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
104	7 83 11 103	mplbasss	$$⊢M\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
105		simplr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i\in M$$
106	104 105	sselid	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
107	106	adantr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\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 {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
108	83 94 23 103 107	psrelbas	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to i:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
109	108	feqmptd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to i=\left(v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(v\right)\right)$$
110	105	adantr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\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 M$$
111	7 11 24 110	mplelsfi	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_{0_R}\left(i\right)$$
112	109 111	eqbrtrrd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_{0_R}\left(\left(v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(v\right)\right)\right)$$
113		ssrab2	$$⊢\left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
114	113	a1i	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
115		fvexd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0_R\in \mathrm{V}$$
116	112 114 115	fmptssfisupp	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_{0_R}\left(\left(v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}⟼i\left(v\right)\right)\right)$$
117		eqid	$$⊢{\cdot }_R={\cdot }_R$$
118	8	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge n\in {\mathrm{Base}}_R\right)\to R\in \mathrm{Ring}$$
119		simpr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge n\in {\mathrm{Base}}_R\right)\to n\in {\mathrm{Base}}_R$$
120	94 117 24 118 119	ringlzd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge n\in {\mathrm{Base}}_R\right)\to 0_R{\cdot }_{R}n=0_R$$
121	108	adantr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to i:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
122		elrabi	$$⊢v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\to v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
123	122	adantl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
124	121 123	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to i\left(v\right)\in {\mathrm{Base}}_R$$
125		simpr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to j\in M$$
126	104 125	sselid	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to j\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
127	126	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to j\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
128	83 94 23 103 127	psrelbas	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to j:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟶{\mathrm{Base}}_R$$
129	69	ad5ant14	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to x\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
130	5	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to I\in V$$
131	49	a1i	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
132	51 123	sselid	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\in \left({{\mathbb{N}}_0}^I\right)$$
133	130 131 132	elmaprd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v:I⟶{\mathbb{N}}_0$$
134		breq1	$$⊢w=v\to \left(w{\le }_f\left(x\circ D\right)\leftrightarrow v{\le }_f\left(x\circ D\right)\right)$$
135		simpr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}$$
136	134 135	elrabrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v{\le }_f\left(x\circ D\right)$$
137	23	psrbagcon	$$⊢\left(x\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\wedge v:I⟶{\mathbb{N}}_0\wedge v{\le }_f\left(x\circ D\right)\right)\to \left(\left(x\circ D\right){-}_{f}v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\wedge \left(\left(x\circ D\right){-}_{f}v\right){\le }_f\left(x\circ D\right)\right)$$
138	129 133 136 137	syl3anc	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(\left(x\circ D\right){-}_{f}v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\wedge \left(\left(x\circ D\right){-}_{f}v\right){\le }_f\left(x\circ D\right)\right)$$
139	138	simpld	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(x\circ D\right){-}_{f}v\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
140	128 139	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to j\left(\left(x\circ D\right){-}_{f}v\right)\in {\mathrm{Base}}_R$$
141	116 120 124 140 115	fsuppssov1	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {finSupp}_{0_R}\left(\left(v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}⟼i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)$$
142		ssidd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
143	8	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to R\in \mathrm{Ring}$$
144	94 117 143 124 140	ringcld	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\in {\mathrm{Base}}_R$$
145		breq1	$$⊢w=y\circ D\to \left(w{\le }_f\left(x\circ D\right)\leftrightarrow \left(y\circ D\right){\le }_f\left(x\circ D\right)\right)$$
146	5	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to I\in V$$
147	9	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to D\in P$$
148	147	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to D\in P$$
149		ssrab2	$$⊢\left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\subseteq \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
150		simpr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}$$
151	149 150	sselid	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
152	151	adantlr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
153	1 2 146 148 152	mplvrpmlem	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\circ D\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
154	49	a1i	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
155	51	a1i	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
156	149 155	sstrid	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\subseteq {{\mathbb{N}}_0}^I$$
157	156	sselda	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\in \left({{\mathbb{N}}_0}^I\right)$$
158	146 154 157	elmaprd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y:I⟶{\mathbb{N}}_0$$
159	158	ffnd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to yFnI$$
160	54	ad4ant14	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\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$$
161	160	adantr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to x:I⟶{\mathbb{N}}_0$$
162	161	ffnd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to xFnI$$
163	62	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to D:I⟶I$$
164		breq1	$$⊢z=y\to \left(z{\le }_{f}x\leftrightarrow y{\le }_{f}x\right)$$
165		simpr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}$$
166	164 165	elrabrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y{\le }_{f}x$$
167	159 162 163 146 146 166	ofrco	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(y\circ D\right){\le }_f\left(x\circ D\right)$$
168	145 153 167	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y\circ D\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}$$
169		breq1	$$⊢z=v\circ D^{-1}\to \left(z{\le }_{f}x\leftrightarrow \left(v\circ D^{-1}\right){\le }_{f}x\right)$$
170		breq1	$$⊢h=v\circ D^{-1}\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(v\circ D^{-1}\right)\right)\right)$$
171	42	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to D^{-1}:I⟶I$$
172	133 171	fcod	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(v\circ D^{-1}\right):I⟶{\mathbb{N}}_0$$
173	131 130 172	elmapdd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\circ D^{-1}\in \left({{\mathbb{N}}_0}^I\right)$$
174		breq1	$$⊢h=v\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(v\right)\right)$$
175	174 123	elrabrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to {finSupp}_0\left(v\right)$$
176	39	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to D:I\underset{1-1\; onto}{⟶}I$$
177		f1of1	$$⊢D^{-1}:I\underset{1-1\; onto}{⟶}I\to D^{-1}:I\underset{1-1}{⟶}I$$
178	176 40 177	3syl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to D^{-1}:I\underset{1-1}{⟶}I$$
179	43	a1i	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to 0\in {\mathbb{N}}_0$$
180	175 178 179 123	fsuppco	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to {finSupp}_0\left(\left(v\circ D^{-1}\right)\right)$$
181	170 173 180	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\circ D^{-1}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
182	133	ffnd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to vFnI$$
183	160	adantr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to x:I⟶{\mathbb{N}}_0$$
184	183	ffnd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to xFnI$$
185	62	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to D:I⟶I$$
186		fnfco	$$⊢\left(xFnI\wedge D:I⟶I\right)\to \left(x\circ D\right)FnI$$
187	184 185 186	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(x\circ D\right)FnI$$
188	182 187 171 130 130 136	ofrco	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(v\circ D^{-1}\right){\le }_f\left(\left(x\circ D\right)\circ D^{-1}\right)$$
189	176 31	syl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to D\circ D^{-1}={\mathrm{I}\upharpoonright }_I$$
190	189	coeq2d	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to x\circ \left(D\circ D^{-1}\right)=x\circ \left({\mathrm{I}\upharpoonright }_I\right)$$
191	183 55	syl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
192	190 191	eqtrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to x\circ \left(D\circ D^{-1}\right)=x$$
193	37 192	eqtrid	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(x\circ D\right)\circ D^{-1}=x$$
194	188 193	breqtrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \left(v\circ D^{-1}\right){\le }_{f}x$$
195	169 181 194	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to v\circ D^{-1}\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}$$
196	133	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to v:I⟶{\mathbb{N}}_0$$
197	158	adantlr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to y:I⟶{\mathbb{N}}_0$$
198	39	ad5antr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to D:I\underset{1-1\; onto}{⟶}I$$
199	196 197 198	cocnvf1o	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(v=y\circ D\leftrightarrow y=v\circ D^{-1}\right)$$
200	195 199	reu6dv	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}\right)\to \exists !y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}v=y\circ D$$
201	93 94 24 98 100 102 141 142 144 168 200	gsummptfsf1o	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)=\underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)\right)$$
202		coeq1	$$⊢t=y\to t\circ D=y\circ D$$
203	202	fveq2d	$$⊢t=y\to i\left(t\circ D\right)=i\left(y\circ D\right)$$
204		oveq2	$$⊢f=i\to DAf=DAi$$
205	105	adantr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to i\in M$$
206		ovexd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to DAi\in \mathrm{V}$$
207	6 204 205 206	fvmptd3	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(i\right)=DAi$$
208	4	a1i	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\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)$$
209		simpr	$$⊢\left(d=D\wedge f=i\right)\to f=i$$
210		coeq2	$$⊢d=D\to x\circ d=x\circ D$$
211	210	adantr	$$⊢\left(d=D\wedge f=i\right)\to x\circ d=x\circ D$$
212	209 211	fveq12d	$$⊢\left(d=D\wedge f=i\right)\to f\left(x\circ d\right)=i\left(x\circ D\right)$$
213	212	mpteq2dv	$$⊢\left(d=D\wedge f=i\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\}⟼i\left(x\circ D\right)\right)$$
214		coeq1	$$⊢x=t\to x\circ D=t\circ D$$
215	214	fveq2d	$$⊢x=t\to i\left(x\circ D\right)=i\left(t\circ D\right)$$
216	215	cbvmptv	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(x\circ D\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)$$
217	213 216	eqtrdi	$$⊢\left(d=D\wedge f=i\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(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)$$
218	217	adantl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge \left(d=D\wedge f=i\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(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)$$
219	147	adantr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to D\in P$$
220	79	a1i	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
221	220	mptexd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)\in \mathrm{V}$$
222	208 218 219 205 221	ovmpod	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to DAi=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)$$
223	207 222	eqtrd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(i\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼i\left(t\circ D\right)\right)$$
224		fvexd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to i\left(y\circ D\right)\in \mathrm{V}$$
225	203 223 151 224	fvmptd4	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(i\right)\left(y\right)=i\left(y\circ D\right)$$
226	225	adantlr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(i\right)\left(y\right)=i\left(y\circ D\right)$$
227		oveq2	$$⊢f=j\to DAf=DAj$$
228		simpr	$$⊢\left(d=D\wedge f=j\right)\to f=j$$
229	210	adantr	$$⊢\left(d=D\wedge f=j\right)\to x\circ d=x\circ D$$
230	228 229	fveq12d	$$⊢\left(d=D\wedge f=j\right)\to f\left(x\circ d\right)=j\left(x\circ D\right)$$
231	230	mpteq2dv	$$⊢\left(d=D\wedge f=j\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\}⟼j\left(x\circ D\right)\right)$$
232	214	fveq2d	$$⊢x=t\to j\left(x\circ D\right)=j\left(t\circ D\right)$$
233	232	cbvmptv	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(x\circ D\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
234	231 233	eqtrdi	$$⊢\left(d=D\wedge f=j\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(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
235	234	adantl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge \left(d=D\wedge f=j\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(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
236		simplr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to j\in M$$
237	220	mptexd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)\in \mathrm{V}$$
238	208 235 219 236 237	ovmpod	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to DAj=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
239	227 238	sylan9eqr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge f=j\right)\to DAf=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
240	239	adantllr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge f=j\right)\to DAf=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
241	125	ad2antrr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to j\in M$$
242	79	a1i	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
243	242	mptexd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)\in \mathrm{V}$$
244	6 240 241 243	fvmptd2	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(j\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼j\left(t\circ D\right)\right)$$
245		coeq1	$$⊢t=x{-}_{f}y\to t\circ D=\left(x{-}_{f}y\right)\circ D$$
246	245	fveq2d	$$⊢t=x{-}_{f}y\to j\left(t\circ D\right)=j\left(\left(x{-}_{f}y\right)\circ D\right)$$
247	246	adantl	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to j\left(t\circ D\right)=j\left(\left(x{-}_{f}y\right)\circ D\right)$$
248	160	ad2antrr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to x:I⟶{\mathbb{N}}_0$$
249	248	ffnd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to xFnI$$
250	5	ad5antr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to I\in V$$
251	49	a1i	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
252	157	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to y\in \left({{\mathbb{N}}_0}^I\right)$$
253	250 251 252	elmaprd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to y:I⟶{\mathbb{N}}_0$$
254	253	ffnd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to yFnI$$
255	62	ad5antr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to D:I⟶I$$
256		inidm	$$⊢I\cap I=I$$
257	249 254 255 250 250 250 256	ofco	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to \left(x{-}_{f}y\right)\circ D=\left(x\circ D\right){-}_f\left(y\circ D\right)$$
258	257	fveq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to j\left(\left(x{-}_{f}y\right)\circ D\right)=j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
259	247 258	eqtrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge t=x{-}_{f}y\right)\to j\left(t\circ D\right)=j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
260		breq1	$$⊢h=x{-}_{f}y\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(x{-}_{f}y\right)\right)\right)$$
261	162 159 146 146 256	offn	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(x{-}_{f}y\right)FnI$$
262	162	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to xFnI$$
263	159	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to yFnI$$
264	146	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to I\in V$$
265		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to a\in I$$
266		fnfvof	$$⊢\left(\left(xFnI\wedge yFnI\right)\wedge \left(I\in V\wedge a\in I\right)\right)\to \left(x{-}_{f}y\right)\left(a\right)=x\left(a\right)-y\left(a\right)$$
267	262 263 264 265 266	syl22anc	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to \left(x{-}_{f}y\right)\left(a\right)=x\left(a\right)-y\left(a\right)$$
268	158	ffvelcdmda	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to y\left(a\right)\in {\mathbb{N}}_0$$
269	161	ffvelcdmda	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to x\left(a\right)\in {\mathbb{N}}_0$$
270		simplr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}$$
271	164 270	elrabrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to y{\le }_{f}x$$
272	263 262 264 271 265	fnfvor	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to y\left(a\right)\le x\left(a\right)$$
273		nn0sub	$$⊢\left(y\left(a\right)\in {\mathbb{N}}_0\wedge x\left(a\right)\in {\mathbb{N}}_0\right)\to \left(y\left(a\right)\le x\left(a\right)\leftrightarrow x\left(a\right)-y\left(a\right)\in {\mathbb{N}}_0\right)$$
274	273	biimpa	$$⊢\left(\left(y\left(a\right)\in {\mathbb{N}}_0\wedge x\left(a\right)\in {\mathbb{N}}_0\right)\wedge y\left(a\right)\le x\left(a\right)\right)\to x\left(a\right)-y\left(a\right)\in {\mathbb{N}}_0$$
275	268 269 272 274	syl21anc	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to x\left(a\right)-y\left(a\right)\in {\mathbb{N}}_0$$
276	267 275	eqeltrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in I\right)\to \left(x{-}_{f}y\right)\left(a\right)\in {\mathbb{N}}_0$$
277	276	ralrimiva	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \forall a\in I\left(x{-}_{f}y\right)\left(a\right)\in {\mathbb{N}}_0$$
278		ffnfv	$$⊢\left(x{-}_{f}y\right):I⟶{\mathbb{N}}_0\leftrightarrow \left(\left(x{-}_{f}y\right)FnI\wedge \forall a\in I\left(x{-}_{f}y\right)\left(a\right)\in {\mathbb{N}}_0\right)$$
279	261 277 278	sylanbrc	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(x{-}_{f}y\right):I⟶{\mathbb{N}}_0$$
280	154 146 279	elmapdd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to x{-}_{f}y\in \left({{\mathbb{N}}_0}^I\right)$$
281		ovexd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to x{-}_{f}y\in \mathrm{V}$$
282	43	a1i	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to 0\in {\mathbb{N}}_0$$
283	162 159 146 146	offun	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \mathrm{Fun}\left(x{-}_{f}y\right)$$
284	23	psrbagfsupp	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\to {finSupp}_0\left(x\right)$$
285	284	ad2antlr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to {finSupp}_0\left(x\right)$$
286		dffn2	$$⊢\left(x{-}_{f}y\right)FnI\leftrightarrow \left(x{-}_{f}y\right):I⟶\mathrm{V}$$
287	261 286	sylib	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(x{-}_{f}y\right):I⟶\mathrm{V}$$
288	162	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to xFnI$$
289	159	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to yFnI$$
290	146	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to I\in V$$
291		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to a\in \left(I\setminus {supp}_0\left(x\right)\right)$$
292	291	eldifad	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to a\in I$$
293	288 289 290 292 266	syl22anc	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to \left(x{-}_{f}y\right)\left(a\right)=x\left(a\right)-y\left(a\right)$$
294	43	a1i	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to 0\in {\mathbb{N}}_0$$
295	288 290 294 291	fvdifsupp	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to x\left(a\right)=0$$
296	158	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y:I⟶{\mathbb{N}}_0$$
297	296 292	ffvelcdmd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y\left(a\right)\in {\mathbb{N}}_0$$
298		simplr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}$$
299	164 298	elrabrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y{\le }_{f}x$$
300	289 288 290 299 292	fnfvor	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y\left(a\right)\le x\left(a\right)$$
301	300 295	breqtrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y\left(a\right)\le 0$$
302		nn0le0eq0	$$⊢y\left(a\right)\in {\mathbb{N}}_0\to \left(y\left(a\right)\le 0\leftrightarrow y\left(a\right)=0\right)$$
303	302	biimpa	$$⊢\left(y\left(a\right)\in {\mathbb{N}}_0\wedge y\left(a\right)\le 0\right)\to y\left(a\right)=0$$
304	297 301 303	syl2anc	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to y\left(a\right)=0$$
305	295 304	oveq12d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to x\left(a\right)-y\left(a\right)=0-0$$
306		0m0e0	$$⊢0-0=0$$
307	306	a1i	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to 0-0=0$$
308	293 305 307	3eqtrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\wedge a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to \left(x{-}_{f}y\right)\left(a\right)=0$$
309	287 308	suppss	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to \left(x{-}_{f}y\right)\mathrm{supp}0\subseteq x\mathrm{supp}0$$
310	281 282 283 285 309	fsuppsssuppgd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to {finSupp}_0\left(\left(x{-}_{f}y\right)\right)$$
311	260 280 310	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to x{-}_{f}y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
312		fvexd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)\in \mathrm{V}$$
313	244 259 311 312	fvmptd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(j\right)\left(x{-}_{f}y\right)=j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
314	226 313	oveq12d	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}\right)\to F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)=i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)$$
315	314	mpteq2dva	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}⟼F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)\right)=\left(y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}⟼i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)\right)$$
316	315	oveq2d	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)\right)=\underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(i\left(y\circ D\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_f\left(y\circ D\right)\right)\right)$$
317	201 316	eqtr4d	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)=\underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)\right)$$
318	317	mpteq2dva	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)\right)\right)$$
319		oveq2	$$⊢f=i{\cdot }_{W}j\to DAf=DA\left(i{\cdot }_{W}j\right)$$
320	4	a1i	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\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)$$
321		simprr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\to f=i{\cdot }_{W}j$$
322	7 11 117 13 23 105 125	mplmul	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i{\cdot }_{W}j=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)\right)$$
323	322	adantr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\to i{\cdot }_{W}j=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)\right)$$
324	321 323	eqtrd	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\to f=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)\right)$$
325	324	adantr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to f=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)\right)$$
326		simpr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to u=x\circ d$$
327		simplrl	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to d=D$$
328	327	adantr	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to d=D$$
329	328	coeq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to x\circ d=x\circ D$$
330	326 329	eqtrd	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to u=x\circ D$$
331	330	breq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to \left(w{\le }_{f}u\leftrightarrow w{\le }_f\left(x\circ D\right)\right)$$
332	331	rabbidv	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}=\left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}$$
333	330	fvoveq1d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to j\left(u{-}_{f}v\right)=j\left(\left(x\circ D\right){-}_{f}v\right)$$
334	333	oveq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)=i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)$$
335	332 334	mpteq12dv	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to \left(v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}⟼i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)=\left(v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}⟼i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)$$
336	335	oveq2d	$$⊢\left(\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=x\circ d\right)\to \underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_{f}u\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(u{-}_{f}v\right)\right)=\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)$$
337	5	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\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$$
338	9	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to D\in P$$
339	327 338	eqeltrd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to d\in P$$
340		simpr	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\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\}$$
341	1 2 337 339 340	mplvrpmlem	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\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\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
342		ovexd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\right)\right)\wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\in \mathrm{V}$$
343	325 336 341 342	fvmptd	$$⊢\left(\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\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)=\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)$$
344	343	mpteq2dva	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge \left(d=D\wedge f=i{\cdot }_{W}j\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\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)$$
345	14	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to W\in \mathrm{Ring}$$
346	11 13 345 105 125	ringcld	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i{\cdot }_{W}j\in M$$
347	79	a1i	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
348	347	mptexd	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)\in \mathrm{V}$$
349	320 344 147 346 348	ovmpod	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to DA\left(i{\cdot }_{W}j\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)$$
350	319 349	sylan9eqr	$$⊢\left(\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\wedge f=i{\cdot }_{W}j\right)\to DAf=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)$$
351	6 350 346 348	fvmptd2	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i{\cdot }_{W}j\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{v\in \left\{w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|w{\le }_f\left(x\circ D\right)\right\}}{{\sum }_R}\left(i\left(v\right){\cdot }_{R}j\left(\left(x\circ D\right){-}_{f}v\right)\right)\right)$$
352	1 2 3 4 5	mplvrpmga	$$⊢\phi \to A\in \left(S\mathrm{GrpAct}M\right)$$
353	2	gaf	$$⊢A\in \left(S\mathrm{GrpAct}M\right)\to A:P\times M⟶M$$
354	352 353	syl	$$⊢\phi \to A:P\times M⟶M$$
355	354	fovcld	$$⊢\left(\phi \wedge D\in P\wedge f\in M\right)\to DAf\in M$$
356	355	3expa	$$⊢\left(\left(\phi \wedge D\in P\right)\wedge f\in M\right)\to DAf\in M$$
357	356	an32s	$$⊢\left(\left(\phi \wedge f\in M\right)\wedge D\in P\right)\to DAf\in M$$
358	9 357	mpidan	$$⊢\left(\phi \wedge f\in M\right)\to DAf\in M$$
359	358 6	fmptd	$$⊢\phi \to F:M⟶M$$
360	359	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F:M⟶M$$
361	360 105	ffvelcdmd	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i\right)\in M$$
362	360 125	ffvelcdmd	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(j\right)\in M$$
363	7 11 117 13 23 361 362	mplmul	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i\right){\cdot }_{W}F\left(j\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\underset{y\in \left\{z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}|z{\le }_{f}x\right\}}{{\sum }_R}\left(F\left(i\right)\left(y\right){\cdot }_{R}F\left(j\right)\left(x{-}_{f}y\right)\right)\right)$$
364	318 351 363	3eqtr4d	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i{\cdot }_{W}j\right)=F\left(i\right){\cdot }_{W}F\left(j\right)$$
365	364	anasss	$$⊢\left(\phi \wedge \left(i\in M\wedge j\in M\right)\right)\to F\left(i{\cdot }_{W}j\right)=F\left(i\right){\cdot }_{W}F\left(j\right)$$
366		eqid	$$⊢{+}_W={+}_W$$
367	1 2 3 4 5 6 7 8 9	mplvrpmmhm	$$⊢\phi \to F\in \left(W\mathrm{MndHom}W\right)$$
368	367	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
369	11 366 366	mhmlin	$$⊢\left(F\in \left(W\mathrm{MndHom}W\right)\wedge i\in M\wedge j\in M\right)\to F\left(i{+}_{W}j\right)=F\left(i\right){+}_{W}F\left(j\right)$$
370	368 105 125 369	syl3anc	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i{+}_{W}j\right)=F\left(i\right){+}_{W}F\left(j\right)$$
371	370	anasss	$$⊢\left(\phi \wedge \left(i\in M\wedge j\in M\right)\right)\to F\left(i{+}_{W}j\right)=F\left(i\right){+}_{W}F\left(j\right)$$
372	11 12 12 13 13 14 14 92 365 11 366 366 359 371	isrhmd	$$⊢\phi \to F\in \left(W\mathrm{RingHom}W\right)$$