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.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
4		psdmplcl.r	$$⊢\phi \to R\in \mathrm{Mnd}$$
5		psdmplcl.x	$$⊢\phi \to X\in I$$
6		psdmplcl.f	$$⊢\phi \to F\in B$$
7		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
9		mndmgm	$$⊢R\in \mathrm{Mnd}\to R\in \mathrm{Mgm}$$
10	4 9	syl	$$⊢\phi \to R\in \mathrm{Mgm}$$
11	1 7 2 8	mplbasss	$$⊢B\subseteq {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
12	11 6	sselid	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
13	7 8 3 10 5 12	psdcl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14		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\}$$
15	7 8 14 3 10 5 12	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)$$
16		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
18	17	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}$$
19	18	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}$$
20		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
21		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)$$
22	21	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)$$
23		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\}$$
24	14	psrbagsn	$$⊢I\in 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\}$$
25	3 24	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\}$$
26	25	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\}$$
27	14	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\}$$
28	23 26 27	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\}$$
29		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)$$
30		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
31	1 30 2 14 6	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$$
32	31	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)$$
33		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)$$
34	28 29 32 33	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)$$
35		eqid	$$⊢0_R=0_R$$
36	1 2 35 6 4	mplelsfi	$$⊢\phi \to {finSupp}_{0_R}\left(F\right)$$
37	28	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\}$$
38		ovex	$$⊢b{-}_f\left(y\in I⟼if\left(y=X,1,0\right)\right)\in \mathrm{V}$$
39		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)$$
40	38 39	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\}$$
41	40	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\}$$
42		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)$$
43	41 42	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)$$
44	43 37	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)$$
45	44	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\}$$
46		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\}$$
47	46	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\}$$
48	14	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$$
49	48	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$$
50	49	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$$
51	50	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 ℂ$$
52		ax-1cn	$$⊢1\in ℂ$$
53		0cn	$$⊢0\in ℂ$$
54	52 53	ifcli	$$⊢if\left(i=X,1,0\right)\in ℂ$$
55	54	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 ℂ$$
56	51 55	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)$$
57	56	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)$$
58		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\}$$
59	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 \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\}$$
60	14	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\}$$
61	58 59 60	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\}$$
62	14	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$$
63	62	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$$
64	61 63	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$$
65		1ex	$$⊢1\in \mathrm{V}$$
66		c0ex	$$⊢0\in \mathrm{V}$$
67	65 66	ifex	$$⊢if\left(y=X,1,0\right)\in \mathrm{V}$$
68		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)$$
69	67 68	fnmpti	$$⊢\left(y\in I⟼if\left(y=X,1,0\right)\right)FnI$$
70	69	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$$
71	3	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 V$$
72		inidm	$$⊢I\cap I=I$$
73	48	ffnd	$$⊢d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to dFnI$$
74	73	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$$
75		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)$$
76		eqeq1	$$⊢y=i\to \left(y=X\leftrightarrow i=X\right)$$
77	76	ifbid	$$⊢y=i\to if\left(y=X,1,0\right)=if\left(i=X,1,0\right)$$
78		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$$
79	65 66	ifex	$$⊢if\left(i=X,1,0\right)\in \mathrm{V}$$
80	79	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}$$
81	68 77 78 80	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)$$
82	74 70 71 71 72 75 81	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)$$
83	64 70 71 71 72 82 81	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)$$
84	49	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)$$
85	57 83 84	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$$
86	28	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\}$$
87	86	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\}$$
88	87 58	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)$$
89		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)$$
90		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)$$
91		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}$$
92	89 90 58 91	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)$$
93	92	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)$$
94		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)$$
95		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}$$
96	39 94 61 95	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)$$
97	88 93 96	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)$$
98		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$$
99	98	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$$
100	85 97 99	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)$$
101	45 47 100	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\}}$$
102		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\}$$
103	37 101 102	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\}$$
104	36 103 20 6	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)$$
105	34 104	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)$$
106	105	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}$$
107		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$$
108		eqid	$$⊢{\cdot }_R={\cdot }_R$$
109	30 108 35	mulgnn0z	$$⊢\left(R\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\right)\to n{\cdot }_R{0}_R=0_R$$
110	4 109	sylan	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n{\cdot }_R{0}_R=0_R$$
111	14	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$$
112	111	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$$
113	5	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$$
114	112 113	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$$
115		peano2nn0	$$⊢k\left(X\right)\in {\mathbb{N}}_0\to k\left(X\right)+1\in {\mathbb{N}}_0$$
116	114 115	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$$
117		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}$$
118	107 110 116 117 20	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$$
119	106 118	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}$$
120	19 20 22 119	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)$$
121	15 120	eqbrtrd	$$⊢\phi \to {finSupp}_{0_R}\left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
122	1 7 8 35 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)$$
123	13 121 122	sylanbrc	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B$$