Theorem psdmplcl

Description: The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025)

	Ref	Expression
Hypotheses	psdmplcl.p	$$⊢P=I\mathrm{mPoly}R$$
	psdmplcl.b	$$⊢B={\mathrm{Base}}_P$$
	psdmplcl.r	$$⊢\phi \to R\in \mathrm{Mnd}$$
	psdmplcl.x	$$⊢\phi \to X\in I$$
	psdmplcl.f	$$⊢\phi \to F\in B$$
Assertion	psdmplcl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		psdmplcl.p	$$⊢P=I\mathrm{mPoly}R$$
2		psdmplcl.b	$$⊢B={\mathrm{Base}}_P$$
3		psdmplcl.r	$$⊢\phi \to R\in \mathrm{Mnd}$$
4		psdmplcl.x	$$⊢\phi \to X\in I$$
5		psdmplcl.f	$$⊢\phi \to F\in B$$
6		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8		mndmgm	$$⊢R\in \mathrm{Mnd}\to R\in \mathrm{Mgm}$$
9	3 8	syl	$$⊢\phi \to R\in \mathrm{Mgm}$$
10	1 6 2 7	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
11	10 5	sselid	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
12	6 7 9 4 11	psdcl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
13		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
14	6 7 13 4 11	psdval	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)$$
15		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
16	15	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
18	17	mptexd	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\in \mathrm{V}$$
19		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
20		funmpt	$$⊢\mathrm{Fun}\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)$$
21	20	a1i	$$⊢\phi \to \mathrm{Fun}\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)$$
22		simpr	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
23		reldmmpl	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$
24	1 2 23	strov2rcl	$$⊢F\in B\to I\in \mathrm{V}$$
25	5 24	syl	$$⊢\phi \to I\in \mathrm{V}$$
26	13	psrbagsn	$$⊢I\in \mathrm{V}\to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
27	25 26	syl	$$⊢\phi \to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
28	27	adantr	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
29	13	psrbagaddcl	$$⊢\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
30	22 28 29	syl2anc	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
31		eqidd	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
32		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
33	1 32 2 13 5	mplelf	$$⊢\phi \to F:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
34	33	feqmptd	$$⊢\phi \to F=\left(z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(z\right)\right)$$
35		fveq2	$$⊢z=k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\to F\left(z\right)=F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
36	30 31 34 35	fmptco	$$⊢\phi \to F\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)$$
37		eqid	$$⊢0_R=0_R$$
38	1 2 37 5	mplelsfi	$$⊢\phi \to {finSupp}_{0_R}\left(F\right)$$
39	30	fmpttd	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
40		ovex	$$⊢b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \mathrm{V}$$
41		eqid	$$⊢\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
42	40 41	fnmpti	$$⊢\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
43	42	a1i	$$⊢\phi \to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
44		dffn3	$$⊢\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\leftrightarrow \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\mathrm{ran}\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
45	43 44	sylib	$$⊢\phi \to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\mathrm{ran}\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
46	45 39	fcod	$$⊢\phi \to \left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\mathrm{ran}\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
47	46	ffnd	$$⊢\phi \to \left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
48		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
49	48	a1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)Fn\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
50	13	psrbagf	$$⊢d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to d:I⟶{\mathbb{N}}_0$$
51	50	adantl	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d:I⟶{\mathbb{N}}_0$$
52	51	ffvelcdmda	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to d\left(i\right)\in {\mathbb{N}}_0$$
53	52	nn0cnd	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to d\left(i\right)\in ℂ$$
54		ax-1cn	$$⊢1\in ℂ$$
55		0cn	$$⊢0\in ℂ$$
56	54 55	ifcli	$$⊢if\left(i=X,1,0\right)\in ℂ$$
57	56	a1i	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to if\left(i=X,1,0\right)\in ℂ$$
58	53 57	pncand	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to d\left(i\right)+if\left(i=X,1,0\right)-if\left(i=X,1,0\right)=d\left(i\right)$$
59	58	mpteq2dva	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(i\in I⟼d\left(i\right)+if\left(i=X,1,0\right)-if\left(i=X,1,0\right)\right)=\left(i\in I⟼d\left(i\right)\right)$$
60		simpr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
61	27	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
62	13	psrbagaddcl	$$⊢\left(d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
63	60 61 62	syl2anc	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
64	13	psrbagf	$$⊢d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):I⟶{\mathbb{N}}_0$$
65	64	ffnd	$$⊢d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)FnI$$
66	63 65	syl	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)FnI$$
67		1ex	$$⊢1\in \mathrm{V}$$
68		c0ex	$$⊢0\in \mathrm{V}$$
69	67 68	ifex	$$⊢if\left(y=X,1,0\right)\in \mathrm{V}$$
70		eqid	$$⊢\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
71	69 70	fnmpti	$$⊢\left(y\in I⟼if\left(y=X,1,0\right)\right)FnI$$
72	71	a1i	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(y\in I⟼if\left(y=X,1,0\right)\right)FnI$$
73	25	adantr	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to I\in \mathrm{V}$$
74		inidm	$$⊢I\cap I=I$$
75	50	ffnd	$$⊢d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to dFnI$$
76	75	adantl	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to dFnI$$
77		eqidd	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to d\left(i\right)=d\left(i\right)$$
78		eqeq1	$$⊢y=i\to \left(y=X\leftrightarrow i=X\right)$$
79	78	ifbid	$$⊢y=i\to if\left(y=X,1,0\right)=if\left(i=X,1,0\right)$$
80		simpr	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to i\in I$$
81	67 68	ifex	$$⊢if\left(i=X,1,0\right)\in \mathrm{V}$$
82	81	a1i	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to if\left(i=X,1,0\right)\in \mathrm{V}$$
83	70 79 80 82	fvmptd3	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to \left(y\in I⟼if\left(y=X,1,0\right)\right)\left(i\right)=if\left(i=X,1,0\right)$$
84	76 72 73 73 74 77 83	ofval	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge i\in I\right)\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(i\right)=d\left(i\right)+if\left(i=X,1,0\right)$$
85	66 72 73 73 74 84 83	offval	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(i\in I⟼d\left(i\right)+if\left(i=X,1,0\right)-if\left(i=X,1,0\right)\right)$$
86	51	feqmptd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d=\left(i\in I⟼d\left(i\right)\right)$$
87	59 85 86	3eqtr4d	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)=d$$
88	30	adantlr	$$⊢\left(\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
89	88	fmpttd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
90	89 60	fvco3d	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\left(d\right)=\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(d\right)\right)$$
91		eqid	$$⊢\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
92		oveq1	$$⊢k=d\to k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)=d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
93		ovexd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \mathrm{V}$$
94	91 92 60 93	fvmptd3	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(d\right)=d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
95	94	fveq2d	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(d\right)\right)=\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)$$
96		oveq1	$$⊢b=d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\to b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)=\left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
97		ovexd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \mathrm{V}$$
98	41 96 63 97	fvmptd3	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)=\left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
99	90 95 98	3eqtrd	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\left(d\right)=\left(d{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right){-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)$$
100		fvresi	$$⊢d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left({\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\left(d\right)=d$$
101	100	adantl	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left({\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\left(d\right)=d$$
102	87 99 101	3eqtr4d	$$⊢\left(\phi \wedge d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\left(d\right)=\left({\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\left(d\right)$$
103	47 49 102	eqfnfvd	$$⊢\phi \to \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)={\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
104		fcof1	$$⊢\left(\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \left(b\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)={\mathrm{I}\upharpoonright }_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\underset{1-1}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
105	39 103 104	syl2anc	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right):\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\underset{1-1}{⟶}\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
106	38 105 19 5	fsuppco	$$⊢\phi \to {finSupp}_{0_R}\left(\left(F\circ \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\right)$$
107	36 106	eqbrtrrd	$$⊢\phi \to {finSupp}_{0_R}\left(\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\right)$$
108	107	fsuppimpd	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R\in \mathrm{Fin}$$
109		ssidd	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R\subseteq \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R$$
110		eqid	$$⊢{\cdot }_R={\cdot }_R$$
111	32 110 37	mulgnn0z	$$⊢\left(R\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\right)\to n{\cdot }_R{0}_R=0_R$$
112	3 111	sylan	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n{\cdot }_R{0}_R=0_R$$
113	13	psrbagf	$$⊢k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to k:I⟶{\mathbb{N}}_0$$
114	113	adantl	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k:I⟶{\mathbb{N}}_0$$
115	4	adantr	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to X\in I$$
116	114 115	ffvelcdmd	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k\left(X\right)\in {\mathbb{N}}_0$$
117		peano2nn0	$$⊢k\left(X\right)\in {\mathbb{N}}_0\to k\left(X\right)+1\in {\mathbb{N}}_0$$
118	116 117	syl	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to k\left(X\right)+1\in {\mathbb{N}}_0$$
119		fvexd	$$⊢\left(\phi \wedge k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\in \mathrm{V}$$
120	109 112 118 119 19	suppssov2	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R\subseteq \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R$$
121	108 120	ssfid	$$⊢\phi \to \left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\mathrm{supp}{0}_R\in \mathrm{Fin}$$
122	18 19 21 121	isfsuppd	$$⊢\phi \to {finSupp}_{0_R}\left(\left(k\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\left(k\left(X\right)+1\right){\cdot }_{R}F\left(k{+}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\right)\right)\right)$$
123	14 122	eqbrtrd	$$⊢\phi \to {finSupp}_{0_R}\left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
124	1 6 7 37 2	mplelbas	$$⊢\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B\leftrightarrow \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{0_R}\left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\right)$$
125	12 123 124	sylanbrc	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B$$