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{CRing}$$
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{CRing}$$
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 \mathrm{algSc}\left(W\right)\left(O\right)=\mathrm{algSc}\left(W\right)\left(0_{\mathrm{Scalar}\left(W\right)}\right)$$
11		eqid	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(W\right)$$
12		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
13	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
14	1	mpllmod	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to W\in \mathrm{LMod}$$
15	5 13 14	syl2anc	$$⊢\phi \to W\in \mathrm{LMod}$$
16	1	mplring	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to W\in \mathrm{Ring}$$
17	5 13 16	syl2anc	$$⊢\phi \to W\in \mathrm{Ring}$$
18	11 12 15 17	ascl0	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(0_{\mathrm{Scalar}\left(W\right)}\right)=0_W$$
19	10 18	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(O\right)=0_W$$
20	2	fveq1i	$$⊢A\left(O\right)=\mathrm{algSc}\left(W\right)\left(O\right)$$
21	19 20 4	3eqtr4g	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{0}$$