Theorem psd1

Description: The derivative of one is zero. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	psd1.s	$$⊢S=I\mathrm{mPwSer}R$$
	psd1.u	$$⊢\underset{\dot{}}{1}=1_S$$
	psd1.z	$$⊢\underset{\dot{}}{0}=0_S$$
	psd1.i	$$⊢\phi \to I\in V$$
	psd1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	psd1.x	$$⊢\phi \to X\in I$$
Assertion	psd1	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		psd1.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psd1.u	$$⊢\underset{\dot{}}{1}=1_S$$
3		psd1.z	$$⊢\underset{\dot{}}{0}=0_S$$
4		psd1.i	$$⊢\phi \to I\in V$$
5		psd1.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		psd1.x	$$⊢\phi \to X\in I$$
7		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
8		eqid	$$⊢{+}_S={+}_S$$
9		eqid	$$⊢{\cdot }_S={\cdot }_S$$
10	1 4 5	psrcrng	$$⊢\phi \to S\in \mathrm{CRing}$$
11	10	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
12	7 2	ringidcl	$$⊢S\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_S$$
13	11 12	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_S$$
14	1 7 8 9 4 5 6 13 13	psdmul	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}{\cdot }_S\underset{\dot{}}{1}\right)=\left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){\cdot }_S\underset{\dot{}}{1}\right){+}_S\left(\underset{\dot{}}{1}{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\right)$$
15	7 9 2 11 13	ringlidmd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_S\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
16	15	fveq2d	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}{\cdot }_S\underset{\dot{}}{1}\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
17	5	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
18	17	grpmgmd	$$⊢\phi \to R\in \mathrm{Mgm}$$
19	1 7 4 18 6 13	psdcl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_S$$
20	7 9 2 11 19	ringridmd	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){\cdot }_S\underset{\dot{}}{1}=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
21	7 9 2 11 19	ringlidmd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
22	20 21	oveq12d	$$⊢\phi \to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){\cdot }_S\underset{\dot{}}{1}\right){+}_S\left(\underset{\dot{}}{1}{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){+}_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
23	14 16 22	3eqtr3rd	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){+}_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
24	10	crnggrpd	$$⊢\phi \to S\in \mathrm{Grp}$$
25	7 8 3	grpid	$$⊢\left(S\in \mathrm{Grp}\wedge \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_S\right)\to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){+}_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\leftrightarrow \underset{\dot{}}{0}=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\right)$$
26	24 19 25	syl2anc	$$⊢\phi \to \left(\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right){+}_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\leftrightarrow \underset{\dot{}}{0}=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)\right)$$
27	23 26	mpbid	$$⊢\phi \to \underset{\dot{}}{0}=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)$$
28	27	eqcomd	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$