Theorem ply1scl0

Description: The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1scl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	ply1scl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ply1scl0.y	$$⊢Y=0_P$$
Assertion	ply1scl0	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=Y$$

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1scl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		ply1scl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		ply1scl0.y	$$⊢Y=0_P$$
5	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
6	5	fveq2d	$$⊢R\in \mathrm{Ring}\to 0_R=0_{\mathrm{Scalar}\left(P\right)}$$
7	3 6	eqtrid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(P\right)}$$
8	7	fveq2d	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=A\left(0_{\mathrm{Scalar}\left(P\right)}\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
10	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
11	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
12	2 9 10 11	ascl0	$$⊢R\in \mathrm{Ring}\to A\left(0_{\mathrm{Scalar}\left(P\right)}\right)=0_P$$
13	8 12	eqtrd	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=0_P$$
14	13 4	eqtr4di	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=Y$$