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		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
49		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\}$$
50	48 49	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)$$
51	50	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$$
52		fcoi1	$$⊢x:I⟶{\mathbb{N}}_0\to x\circ \left({\mathrm{I}\upharpoonright }_I\right)=x$$
53	51 52	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$$
54	53	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$$
55	34 47 54	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\}$$
56		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\}$$
57	56	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$$
58		f1of	$$⊢D:I\underset{1-1\; onto}{⟶}I\to D:I⟶I$$
59	9 30 58	3syl	$$⊢\phi \to D:I⟶I$$
60	59 44	constcof	$$⊢\phi \to \left(I\times \left\{0\right\}\right)\circ D=I\times \left\{0\right\}$$
61	60	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\}$$
62	57 61	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\}$$
63	55 62	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)$$
64	28 63	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)$$
65	64	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)$$
66	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$$
67	1 2 66 29 49	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\}$$
68		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}$$
69		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}$$
70	68 69	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}$$
71	27 65 67 70	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)$$
72	71	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)$$
73	21 72	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)$$
74	73	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)$$
75	11 12 14	ringidcld	$$⊢\phi \to 1_W\in M$$
76		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
77	76	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
78	77	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
79	78	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}$$
80	16 74 9 75 79	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)$$
81		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
82		eqid	$$⊢1_{\left(I\mathrm{mPwSer}R\right)}=1_{\left(I\mathrm{mPwSer}R\right)}$$
83	81 5 8 23 24 25 82	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)$$
84	81 7 11 5 8	mplsubrg	$$⊢\phi \to M\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
85	7 81 11	mplval2	$$⊢W=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}M$$
86	85 82	subrg1	$$⊢M\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)\to 1_{\left(I\mathrm{mPwSer}R\right)}=1_W$$
87	84 86	syl	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}=1_W$$
88	80 83 87	3eqtr2d	$$⊢\phi \to DA{1}_W=1_W$$
89	15 88	sylan9eqr	$$⊢\left(\phi \wedge f=1_W\right)\to DAf=1_W$$
90	6 89 75 75	fvmptd2	$$⊢\phi \to F\left(1_W\right)=1_W$$
91		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)$$
92		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
93		fveq2	$$⊢v=y\circ D\to i\left(v\right)=i\left(y\circ D\right)$$
94		oveq2	$$⊢v=y\circ D\to \left(x\circ D\right){-}_{f}v=\left(x\circ D\right){-}_f\left(y\circ D\right)$$
95	94	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)$$
96	93 95	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)$$
97	8	ringcmnd	$$⊢\phi \to R\in \mathrm{CMnd}$$
98	97	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}$$
99	77	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}$$
100	99	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}$$
101		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
102	7 81 11 101	mplbasss	$$⊢M\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
103		simplr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i\in M$$
104	102 103	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)}$$
105	104	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)}$$
106	81 92 23 101 105	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$$
107	106	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)$$
108	103	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$$
109	7 11 24 108	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)$$
110	107 109	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)$$
111		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\}$$
112	111	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\}$$
113		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}$$
114	110 112 113	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)$$
115		eqid	$$⊢{\cdot }_R={\cdot }_R$$
116	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}$$
117		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$$
118	92 115 24 116 117	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$$
119	106	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$$
120		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\}$$
121	120	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\}$$
122	119 121	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$$
123		simpr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to j\in M$$
124	102 123	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)}$$
125	124	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)}$$
126	81 92 23 101 125	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$$
127	67	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\}$$
128	48 121	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)$$
129	128	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$$
130		breq1	$$⊢w=v\to \left(w{\le }_f\left(x\circ D\right)\leftrightarrow v{\le }_f\left(x\circ D\right)\right)$$
131		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\}$$
132	130 131	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)$$
133	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)$$
134	127 129 132 133	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)$$
135	134	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\}$$
136	126 135	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$$
137	114 118 122 136 113	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)$$
138		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$$
139	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}$$
140	92 115 139 122 136	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$$
141		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)$$
142	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$$
143	9	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to D\in P$$
144	143	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$$
145		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\}$$
146		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\}$$
147	145 146	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\}$$
148	147	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\}$$
149	1 2 142 144 148	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\}$$
150	48	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$$
151	145 150	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$$
152	151	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)$$
153	152	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$$
154	153	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$$
155	51	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$$
156	155	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$$
157	156	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$$
158	59	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$$
159		breq1	$$⊢z=y\to \left(z{\le }_{f}x\leftrightarrow y{\le }_{f}x\right)$$
160		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\}$$
161	159 160	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$$
162	154 157 158 142 142 161	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)$$
163	141 149 162	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\}$$
164		breq1	$$⊢z=v\circ D^{-1}\to \left(z{\le }_{f}x\leftrightarrow \left(v\circ D^{-1}\right){\le }_{f}x\right)$$
165		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)$$
166		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
167	166	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}$$
168	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$$
169	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$$
170	129 169	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$$
171	167 168 170	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)$$
172		breq1	$$⊢h=v\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(v\right)\right)$$
173	172 121	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)$$
174	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$$
175		f1of1	$$⊢D^{-1}:I\underset{1-1\; onto}{⟶}I\to D^{-1}:I\underset{1-1}{⟶}I$$
176	174 40 175	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$$
177	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$$
178	173 176 177 121	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)$$
179	165 171 178	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\}$$
180	129	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$$
181	155	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$$
182	181	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$$
183	59	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$$
184		fnfco	$$⊢\left(xFnI\wedge D:I⟶I\right)\to \left(x\circ D\right)FnI$$
185	182 183 184	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$$
186	180 185 169 168 168 132	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)$$
187	174 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$$
188	187	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)$$
189	181 52	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$$
190	188 189	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$$
191	37 190	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$$
192	186 191	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$$
193	164 179 192	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\}$$
194	129	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$$
195	153	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$$
196	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$$
197	194 195 196	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)$$
198	193 197	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$$
199	91 92 24 96 98 100 137 138 140 163 198	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)$$
200		coeq1	$$⊢t=y\to t\circ D=y\circ D$$
201	200	fveq2d	$$⊢t=y\to i\left(t\circ D\right)=i\left(y\circ D\right)$$
202		oveq2	$$⊢f=i\to DAf=DAi$$
203	103	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$$
204		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}$$
205	6 202 203 204	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$$
206	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)$$
207		simpr	$$⊢\left(d=D\wedge f=i\right)\to f=i$$
208		coeq2	$$⊢d=D\to x\circ d=x\circ D$$
209	208	adantr	$$⊢\left(d=D\wedge f=i\right)\to x\circ d=x\circ D$$
210	207 209	fveq12d	$$⊢\left(d=D\wedge f=i\right)\to f\left(x\circ d\right)=i\left(x\circ D\right)$$
211	210	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)$$
212		coeq1	$$⊢x=t\to x\circ D=t\circ D$$
213	212	fveq2d	$$⊢x=t\to i\left(x\circ D\right)=i\left(t\circ D\right)$$
214	213	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)$$
215	211 214	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)$$
216	215	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)$$
217	143	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$$
218	77	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}$$
219	218	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}$$
220	206 216 217 203 219	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)$$
221	205 220	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)$$
222		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}$$
223	201 221 147 222	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)$$
224	223	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)$$
225		oveq2	$$⊢f=j\to DAf=DAj$$
226		simpr	$$⊢\left(d=D\wedge f=j\right)\to f=j$$
227	208	adantr	$$⊢\left(d=D\wedge f=j\right)\to x\circ d=x\circ D$$
228	226 227	fveq12d	$$⊢\left(d=D\wedge f=j\right)\to f\left(x\circ d\right)=j\left(x\circ D\right)$$
229	228	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)$$
230	212	fveq2d	$$⊢x=t\to j\left(x\circ D\right)=j\left(t\circ D\right)$$
231	230	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)$$
232	229 231	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)$$
233	232	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)$$
234		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$$
235	218	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}$$
236	206 233 217 234 235	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)$$
237	225 236	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)$$
238	237	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)$$
239	123	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$$
240	77	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}$$
241	240	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}$$
242	6 238 239 241	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)$$
243		coeq1	$$⊢t=x{-}_{f}y\to t\circ D=\left(x{-}_{f}y\right)\circ D$$
244	243	fveq2d	$$⊢t=x{-}_{f}y\to j\left(t\circ D\right)=j\left(\left(x{-}_{f}y\right)\circ D\right)$$
245	244	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)$$
246	155	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$$
247	246	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$$
248	152	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)$$
249	248	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$$
250	249	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$$
251	59	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$$
252	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$$
253		inidm	$$⊢I\cap I=I$$
254	247 250 251 252 252 252 253	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)$$
255	254	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)$$
256	245 255	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)$$
257		breq1	$$⊢h=x{-}_{f}y\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(x{-}_{f}y\right)\right)\right)$$
258	166	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}$$
259	157 154 142 142 253	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$$
260	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 a\in I\right)\to xFnI$$
261	154	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$$
262	142	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$$
263		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$$
264		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)$$
265	260 261 262 263 264	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)$$
266	153	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$$
267	156	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$$
268		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\}$$
269	159 268	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$$
270	261 260 262 269 263	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)$$
271		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)$$
272	271	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$$
273	266 267 270 272	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$$
274	265 273	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$$
275	274	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$$
276		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)$$
277	259 275 276	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$$
278	258 142 277	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)$$
279		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}$$
280	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$$
281	157 154 142 142	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)$$
282	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)$$
283	282	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)$$
284		dffn2	$$⊢\left(x{-}_{f}y\right)FnI\leftrightarrow \left(x{-}_{f}y\right):I⟶\mathrm{V}$$
285	259 284	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}$$
286	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 a\in \left(I\setminus {supp}_0\left(x\right)\right)\right)\to xFnI$$
287	154	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$$
288	142	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$$
289		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)$$
290	289	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$$
291	286 287 288 290 264	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)$$
292	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$$
293	286 288 292 289	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$$
294	153	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$$
295	294 290	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$$
296		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\}$$
297	159 296	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$$
298	287 286 288 297 290	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)$$
299	298 293	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$$
300		nn0le0eq0	$$⊢y\left(a\right)\in {\mathbb{N}}_0\to \left(y\left(a\right)\le 0\leftrightarrow y\left(a\right)=0\right)$$
301	300	biimpa	$$⊢\left(y\left(a\right)\in {\mathbb{N}}_0\wedge y\left(a\right)\le 0\right)\to y\left(a\right)=0$$
302	295 299 301	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$$
303	293 302	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$$
304		0m0e0	$$⊢0-0=0$$
305	304	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$$
306	291 303 305	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$$
307	285 306	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$$
308	279 280 281 283 307	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)$$
309	257 278 308	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\}$$
310		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}$$
311	242 256 309 310	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)$$
312	224 311	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)$$
313	312	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)$$
314	313	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)$$
315	199 314	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)$$
316	315	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)$$
317		oveq2	$$⊢f=i{\cdot }_{W}j\to DAf=DA\left(i{\cdot }_{W}j\right)$$
318	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)$$
319		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$$
320	7 11 115 13 23 103 123	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)$$
321	320	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)$$
322	319 321	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)$$
323	322	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)$$
324		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$$
325		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$$
326	325	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$$
327	326	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$$
328	324 327	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$$
329	328	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)$$
330	329	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\}$$
331	328	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)$$
332	331	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)$$
333	330 332	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)$$
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 \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)$$
335	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$$
336	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$$
337	325 336	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$$
338		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\}$$
339	1 2 335 337 338	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\}$$
340		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}$$
341	323 334 339 340	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)$$
342	341	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)$$
343	14	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to W\in \mathrm{Ring}$$
344	11 13 343 103 123	ringcld	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to i{\cdot }_{W}j\in M$$
345	77	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}$$
346	345	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}$$
347	318 342 143 344 346	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)$$
348	317 347	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)$$
349	6 348 344 346	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)$$
350	1 2 3 4 5	mplvrpmga	$$⊢\phi \to A\in \left(S\mathrm{GrpAct}M\right)$$
351	2	gaf	$$⊢A\in \left(S\mathrm{GrpAct}M\right)\to A:P\times M⟶M$$
352	350 351	syl	$$⊢\phi \to A:P\times M⟶M$$
353	352	fovcld	$$⊢\left(\phi \wedge D\in P\wedge f\in M\right)\to DAf\in M$$
354	353	3expa	$$⊢\left(\left(\phi \wedge D\in P\right)\wedge f\in M\right)\to DAf\in M$$
355	354	an32s	$$⊢\left(\left(\phi \wedge f\in M\right)\wedge D\in P\right)\to DAf\in M$$
356	9 355	mpidan	$$⊢\left(\phi \wedge f\in M\right)\to DAf\in M$$
357	356 6	fmptd	$$⊢\phi \to F:M⟶M$$
358	357	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F:M⟶M$$
359	358 103	ffvelcdmd	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(i\right)\in M$$
360	358 123	ffvelcdmd	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\left(j\right)\in M$$
361	7 11 115 13 23 359 360	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)$$
362	316 349 361	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)$$
363	362	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)$$
364		eqid	$$⊢{+}_W={+}_W$$
365	1 2 3 4 5 6 7 8 9	mplvrpmmhm	$$⊢\phi \to F\in \left(W\mathrm{MndHom}W\right)$$
366	365	ad2antrr	$$⊢\left(\left(\phi \wedge i\in M\right)\wedge j\in M\right)\to F\in \left(W\mathrm{MndHom}W\right)$$
367	11 364 364	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)$$
368	366 103 123 367	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)$$
369	368	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)$$
370	11 12 12 13 13 14 14 90 363 11 364 364 357 369	isrhmd	$$⊢\phi \to F\in \left(W\mathrm{RingHom}W\right)$$