Theorem mplascl1

Description: The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		mplascl1.w	$$⊢W=I\mathrm{mPoly}R$$
2		mplascl1.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
3		mplascl1.o	$$⊢O=1_R$$
4		mplascl1.1	$$⊢\underset{\dot{}}{1}=1_W$$
5		mplascl1.i	$$⊢\phi \to I\in V$$
6		mplascl1.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 1_R=1_{\mathrm{Scalar}\left(W\right)}$$
9	3 8	eqtrid	$$⊢\phi \to O=1_{\mathrm{Scalar}\left(W\right)}$$
10	9	fveq2d	$$⊢\phi \to A\left(O\right)=A\left(1_{\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	ascl1	$$⊢\phi \to A\left(1_{\mathrm{Scalar}\left(W\right)}\right)=1_W$$
15	10 14	eqtrd	$$⊢\phi \to A\left(O\right)=1_W$$
16	15 4	eqtr4di	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{1}$$