Theorem psdascl

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

	Ref	Expression
Hypotheses	psdascl.s	$$⊢S=I\mathrm{mPwSer}R$$
	psdascl.z	$$⊢\underset{\dot{}}{0}=0_S$$
	psdascl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
	psdascl.b	$$⊢B={\mathrm{Base}}_R$$
	psdascl.i	$$⊢\phi \to I\in V$$
	psdascl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	psdascl.x	$$⊢\phi \to X\in I$$
	psdascl.c	$$⊢\phi \to C\in B$$
Assertion	psdascl	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(A\left(C\right)\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		psdascl.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psdascl.z	$$⊢\underset{\dot{}}{0}=0_S$$
3		psdascl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
4		psdascl.b	$$⊢B={\mathrm{Base}}_R$$
5		psdascl.i	$$⊢\phi \to I\in V$$
6		psdascl.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		psdascl.x	$$⊢\phi \to X\in I$$
8		psdascl.c	$$⊢\phi \to C\in B$$
9	1 5 6	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$
10	9	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
11	4 10	eqtrid	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
12	8 11	eleqtrd	$$⊢\phi \to C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
13		eqid	$$⊢\mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(S\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
15		eqid	$$⊢{\cdot }_S={\cdot }_S$$
16		eqid	$$⊢1_S=1_S$$
17	3 13 14 15 16	asclval	$$⊢C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}\to A\left(C\right)=C{\cdot }_S{1}_S$$
18	12 17	syl	$$⊢\phi \to A\left(C\right)=C{\cdot }_S{1}_S$$
19	18	fveq2d	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(A\left(C\right)\right)=\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(C{\cdot }_S{1}_S\right)$$
20		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
21	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
22	1 5 21	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
23	20 16	ringidcl	$$⊢S\in \mathrm{Ring}\to 1_S\in {\mathrm{Base}}_S$$
24	22 23	syl	$$⊢\phi \to 1_S\in {\mathrm{Base}}_S$$
25	1 20 15 4 5 6 7 24 8	psdvsca	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(C{\cdot }_S{1}_S\right)=C{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1_S\right)$$
26	1 16 2 5 6 7	psd1	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1_S\right)=\underset{\dot{}}{0}$$
27	26	oveq2d	$$⊢\phi \to C{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1_S\right)=C{\cdot }_S\underset{\dot{}}{0}$$
28	1 5 21	psrlmod	$$⊢\phi \to S\in \mathrm{LMod}$$
29	13 15 14 2	lmodvs0	$$⊢\left(S\in \mathrm{LMod}\wedge C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}\right)\to C{\cdot }_S\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
30	28 12 29	syl2anc	$$⊢\phi \to C{\cdot }_S\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
31	27 30	eqtrd	$$⊢\phi \to C{\cdot }_S\left(I\mathrm{mPSDer}R\right)\left(X\right)\left(1_S\right)=\underset{\dot{}}{0}$$
32	19 25 31	3eqtrd	$$⊢\phi \to \left(I\mathrm{mPSDer}R\right)\left(X\right)\left(A\left(C\right)\right)=\underset{\dot{}}{0}$$