Theorem mplascl0

Description: The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Hypotheses	mplascl0.w	$$⊢W=I\mathrm{mPoly}R$$
	mplascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	mplascl0.o	$$⊢O=0_R$$
	mplascl0.0	$$⊢\underset{\dot{}}{0}=0_W$$
	mplascl0.i	$$⊢\phi \to I\in V$$
	mplascl0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mplascl0	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mplascl0.w	$$⊢W=I\mathrm{mPoly}R$$
2		mplascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
3		mplascl0.o	$$⊢O=0_R$$
4		mplascl0.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		mplascl0.i	$$⊢\phi \to I\in V$$
6		mplascl0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7	1 5 6	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(W\right)$$
8	7	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(W\right)}$$
9	3 8	eqtrid	$$⊢\phi \to O=0_{\mathrm{Scalar}\left(W\right)}$$
10	9	fveq2d	$$⊢\phi \to A\left(O\right)=A\left(0_{\mathrm{Scalar}\left(W\right)}\right)$$
11		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
12	1 5 6	mpllmodd	$$⊢\phi \to W\in \mathrm{LMod}$$
13	1 5 6	mplringd	$$⊢\phi \to W\in \mathrm{Ring}$$
14	2 11 12 13	ascl0	$$⊢\phi \to A\left(0_{\mathrm{Scalar}\left(W\right)}\right)=0_W$$
15	10 14	eqtrd	$$⊢\phi \to A\left(O\right)=0_W$$
16	15 4	eqtr4di	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{0}$$