Theorem psdpw

Description: Power rule for partial derivative of power series. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	psdpw.s	$$⊢S=I\mathrm{mPwSer}R$$
	psdpw.b	$$⊢B={\mathrm{Base}}_S$$
	psdpw.g	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	psdpw.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
	psdpw.m	$$⊢M={\mathrm{mulGrp}}_S$$
	psdpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
	psdpw.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	psdpw.x	$$⊢\phi \to X\in I$$
	psdpw.f	$$⊢\phi \to F\in B$$
	psdpw.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	psdpw	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(N\underset{\dot{}}{\times }F\right)=\left(N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		psdpw.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psdpw.b	$$⊢B={\mathrm{Base}}_S$$
3		psdpw.g	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
4		psdpw.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_S$$
5		psdpw.m	$$⊢M={\mathrm{mulGrp}}_S$$
6		psdpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_M$$
7		psdpw.r	$$⊢\phi \to R\in \mathrm{CRing}$$
8		psdpw.x	$$⊢\phi \to X\in I$$
9		psdpw.f	$$⊢\phi \to F\in B$$
10		psdpw.n	$$⊢\phi \to N\in \mathbb{N}$$
11		fvoveq1	$$⊢n=1\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1\underset{\dot{}}{\times }F\right)$$
12		id	$$⊢n=1\to n=1$$
13		oveq1	$$⊢n=1\to n-1=1-1$$
14		1m1e0	$$⊢1-1=0$$
15	13 14	eqtrdi	$$⊢n=1\to n-1=0$$
16	15	oveq1d	$$⊢n=1\to \left(n-1\right)\underset{\dot{}}{\times }F=0\underset{\dot{}}{\times }F$$
17	12 16	oveq12d	$$⊢n=1\to n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)=1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)$$
18	17	oveq1d	$$⊢n=1\to \left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
19	11 18	eqeq12d	$$⊢n=1\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\leftrightarrow \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1\underset{\dot{}}{\times }F\right)=\left(1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
20		fvoveq1	$$⊢n=m\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)$$
21		id	$$⊢n=m\to n=m$$
22		oveq1	$$⊢n=m\to n-1=m-1$$
23	22	oveq1d	$$⊢n=m\to \left(n-1\right)\underset{\dot{}}{\times }F=\left(m-1\right)\underset{\dot{}}{\times }F$$
24	21 23	oveq12d	$$⊢n=m\to n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)=m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)$$
25	24	oveq1d	$$⊢n=m\to \left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
26	20 25	eqeq12d	$$⊢n=m\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\leftrightarrow \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
27		fvoveq1	$$⊢n=m+1\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m+1\right)\underset{\dot{}}{\times }F\right)$$
28		id	$$⊢n=m+1\to n=m+1$$
29		oveq1	$$⊢n=m+1\to n-1=m+1-1$$
30	29	oveq1d	$$⊢n=m+1\to \left(n-1\right)\underset{\dot{}}{\times }F=\left(m+1-1\right)\underset{\dot{}}{\times }F$$
31	28 30	oveq12d	$$⊢n=m+1\to n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)=\left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)$$
32	31	oveq1d	$$⊢n=m+1\to \left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
33	27 32	eqeq12d	$$⊢n=m+1\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\leftrightarrow \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m+1\right)\underset{\dot{}}{\times }F\right)=\left(\left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
34		fvoveq1	$$⊢n=N\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(N\underset{\dot{}}{\times }F\right)$$
35		id	$$⊢n=N\to n=N$$
36		oveq1	$$⊢n=N\to n-1=N-1$$
37	36	oveq1d	$$⊢n=N\to \left(n-1\right)\underset{\dot{}}{\times }F=\left(N-1\right)\underset{\dot{}}{\times }F$$
38	35 37	oveq12d	$$⊢n=N\to n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)=N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)$$
39	38	oveq1d	$$⊢n=N\to \left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
40	34 39	eqeq12d	$$⊢n=N\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(n\underset{\dot{}}{\times }F\right)=\left(n\underset{\dot{}}{·}\left(\left(n-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\leftrightarrow \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(N\underset{\dot{}}{\times }F\right)=\left(N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
41		eqid	$$⊢1_S=1_S$$
42		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
43	42 1 2	elbasov	$$⊢F\in B\to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
44	9 43	syl	$$⊢\phi \to \left(I\in \mathrm{V}\wedge R\in \mathrm{V}\right)$$
45	44	simpld	$$⊢\phi \to I\in \mathrm{V}$$
46	1 45 7	psrcrng	$$⊢\phi \to S\in \mathrm{CRing}$$
47	46	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
48	7	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
49	48	grpmgmd	$$⊢\phi \to R\in \mathrm{Mgm}$$
50	1 2 49 8 9	psdcl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B$$
51	2 4 41 47 50	ringlidmd	$$⊢\phi \to 1_S\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
52	5 2	mgpbas	$$⊢B={\mathrm{Base}}_M$$
53	5 41	ringidval	$$⊢1_S=0_M$$
54	52 53 6	mulg0	$$⊢F\in B\to 0\underset{\dot{}}{\times }F=1_S$$
55	9 54	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }F=1_S$$
56	55	oveq2d	$$⊢\phi \to 1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)=1\underset{\dot{}}{·}{1}_S$$
57	2 41 47	ringidcld	$$⊢\phi \to 1_S\in B$$
58	2 3	mulg1	$$⊢1_S\in B\to 1\underset{\dot{}}{·}{1}_S=1_S$$
59	57 58	syl	$$⊢\phi \to 1\underset{\dot{}}{·}{1}_S=1_S$$
60	56 59	eqtrd	$$⊢\phi \to 1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)=1_S$$
61	60	oveq1d	$$⊢\phi \to \left(1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=1_S\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
62	52 6	mulg1	$$⊢F\in B\to 1\underset{\dot{}}{\times }F=F$$
63	9 62	syl	$$⊢\phi \to 1\underset{\dot{}}{\times }F=F$$
64	63	fveq2d	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
65	51 61 64	3eqtr4rd	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1\underset{\dot{}}{\times }F\right)=\left(1\underset{\dot{}}{·}\left(0\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
66		simpr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
67	66	oveq1d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F=\left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\underset{\dot{}}{\bullet }F$$
68	46	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to S\in \mathrm{CRing}$$
69	46	crnggrpd	$$⊢\phi \to S\in \mathrm{Grp}$$
70	69	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to S\in \mathrm{Grp}$$
71		simpr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\in \mathbb{N}$$
72	71	nnzd	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\in \mathbb{Z}$$
73	47	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to S\in \mathrm{Ring}$$
74	5	ringmgp	$$⊢S\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
75	73 74	syl	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to M\in \mathrm{Mnd}$$
76		nnm1nn0	$$⊢m\in \mathbb{N}\to m-1\in {\mathbb{N}}_0$$
77	76	adantl	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m-1\in {\mathbb{N}}_0$$
78	9	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to F\in B$$
79	52 6 75 77 78	mulgnn0cld	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m-1\right)\underset{\dot{}}{\times }F\in B$$
80	2 3 70 72 79	mulgcld	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\in B$$
81	50	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\in B$$
82	2 4 68 80 81 78	crng32d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\underset{\dot{}}{\bullet }F=\left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
83	82	adantr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\underset{\dot{}}{\bullet }F=\left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
84	2 3 4	mulgass2	$$⊢\left(S\in \mathrm{Ring}\wedge \left(m\in \mathbb{Z}\wedge \left(m-1\right)\underset{\dot{}}{\times }F\in B\wedge F\in B\right)\right)\to \left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F=m\underset{\dot{}}{·}\left(\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)$$
85	73 72 79 78 84	syl13anc	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F=m\underset{\dot{}}{·}\left(\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)$$
86	5 4	mgpplusg	$$⊢\underset{\dot{}}{\bullet }={+}_M$$
87	52 6 86	mulgnn0p1	$$⊢\left(M\in \mathrm{Mnd}\wedge m-1\in {\mathbb{N}}_0\wedge F\in B\right)\to \left(m-1+1\right)\underset{\dot{}}{\times }F=\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F$$
88	75 77 78 87	syl3anc	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m-1+1\right)\underset{\dot{}}{\times }F=\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F$$
89	71	nncnd	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\in ℂ$$
90		npcan1	$$⊢m\in ℂ\to m-1+1=m$$
91	89 90	syl	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m-1+1=m$$
92	91	oveq1d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m-1+1\right)\underset{\dot{}}{\times }F=m\underset{\dot{}}{\times }F$$
93	88 92	eqtr3d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F=m\underset{\dot{}}{\times }F$$
94	93	oveq2d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\underset{\dot{}}{·}\left(\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)=m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)$$
95	85 94	eqtrd	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F=m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)$$
96	95	oveq1d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
97	96	adantr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
98	67 83 97	3eqtrd	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F=\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
99	98	oveq1d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)=\left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
100		eqid	$$⊢{+}_S={+}_S$$
101	7	ad2antrr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to R\in \mathrm{CRing}$$
102	8	ad2antrr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to X\in I$$
103	47 74	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
104		mndmgm	$$⊢M\in \mathrm{Mnd}\to M\in \mathrm{Mgm}$$
105	103 104	syl	$$⊢\phi \to M\in \mathrm{Mgm}$$
106	105	adantr	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to M\in \mathrm{Mgm}$$
107	52 6	mulgnncl	$$⊢\left(M\in \mathrm{Mgm}\wedge m\in \mathbb{N}\wedge F\in B\right)\to m\underset{\dot{}}{\times }F\in B$$
108	106 71 78 107	syl3anc	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\underset{\dot{}}{\times }F\in B$$
109	108	adantr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to m\underset{\dot{}}{\times }F\in B$$
110	9	ad2antrr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to F\in B$$
111	1 2 100 4 101 102 109 110	psdmul	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)=\left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
112	2 3 100	mulgnnp1	$$⊢\left(m\in \mathbb{N}\wedge m\underset{\dot{}}{\times }F\in B\right)\to \left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right){+}_S\left(m\underset{\dot{}}{\times }F\right)$$
113	71 108 112	syl2anc	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right){+}_S\left(m\underset{\dot{}}{\times }F\right)$$
114	113	oveq1d	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right){+}_S\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
115	2 3 70 72 108	mulgcld	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\in B$$
116	2 100 4 73 115 108 81	ringdird	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right){+}_S\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
117	114 116	eqtrd	$$⊢\left(\phi \wedge m\in \mathbb{N}\right)\to \left(\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
118	117	adantr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right){+}_S\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)$$
119	99 111 118	3eqtr4d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)=\left(\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
120		simplr	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to m\in \mathbb{N}$$
121	52 6 86	mulgnnp1	$$⊢\left(m\in \mathbb{N}\wedge F\in B\right)\to \left(m+1\right)\underset{\dot{}}{\times }F=\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F$$
122	120 110 121	syl2anc	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(m+1\right)\underset{\dot{}}{\times }F=\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F$$
123	122	fveq2d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m+1\right)\underset{\dot{}}{\times }F\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m\underset{\dot{}}{\times }F\right)\underset{\dot{}}{\bullet }F\right)$$
124	120	nncnd	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to m\in ℂ$$
125		pncan1	$$⊢m\in ℂ\to m+1-1=m$$
126	124 125	syl	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to m+1-1=m$$
127	126	oveq1d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(m+1-1\right)\underset{\dot{}}{\times }F=m\underset{\dot{}}{\times }F$$
128	127	oveq2d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)=\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)$$
129	128	oveq1d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(\left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)=\left(\left(m+1\right)\underset{\dot{}}{·}\left(m\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
130	119 123 129	3eqtr4d	$$⊢\left(\left(\phi \wedge m\in \mathbb{N}\right)\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(m\underset{\dot{}}{\times }F\right)=\left(m\underset{\dot{}}{·}\left(\left(m-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\left(m+1\right)\underset{\dot{}}{\times }F\right)=\left(\left(m+1\right)\underset{\dot{}}{·}\left(\left(m+1-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
131	19 26 33 40 65 130	nnindd	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(N\underset{\dot{}}{\times }F\right)=\left(N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$
132	10 131	mpdan	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(N\underset{\dot{}}{\times }F\right)=\left(N\underset{\dot{}}{·}\left(\left(N-1\right)\underset{\dot{}}{\times }F\right)\right)\underset{\dot{}}{\bullet }\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(F\right)$$