Theorem ply1ascl0

Description: The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025)

	Ref	Expression
Hypotheses	ply1ascl0.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	ply1ascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	ply1ascl0.o	$$⊢O=0_R$$
	ply1ascl0.1	$$⊢\underset{\dot{}}{0}=0_W$$
	ply1ascl0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	ply1ascl0	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		ply1ascl0.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
2		ply1ascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
3		ply1ascl0.o	$$⊢O=0_R$$
4		ply1ascl0.1	$$⊢\underset{\dot{}}{0}=0_W$$
5		ply1ascl0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(W\right)$$
7	5 6	syl	$$⊢\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	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{LMod}$$
14	5 13	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
15	1	ply1ring	$$⊢R\in \mathrm{Ring}\to W\in \mathrm{Ring}$$
16	5 15	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
17	11 12 14 16	ascl0	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(0_{\mathrm{Scalar}\left(W\right)}\right)=0_W$$
18	10 17	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(O\right)=0_W$$
19	2	fveq1i	$$⊢A\left(O\right)=\mathrm{algSc}\left(W\right)\left(O\right)$$
20	18 19 4	3eqtr4g	$$⊢\phi \to A\left(O\right)=\underset{\dot{}}{0}$$