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		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
7	1	ply1sca2	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$
8		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
9	8 5	strfvi	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{I}\left(R\right)}$$
10		eqid	$$⊢{\cdot }_P={\cdot }_P$$
11		eqid	$$⊢1_P=1_P$$
12	2 7 9 10 11	asclval	$$⊢\underset{\dot{}}{0}\in {\mathrm{Base}}_R\to A\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}{\cdot }_P{1}_P$$
13	6 12	syl	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}{\cdot }_P{1}_P$$
14		fvi	$$⊢R\in \mathrm{Ring}\to \mathrm{I}\left(R\right)=R$$
15	14	fveq2d	$$⊢R\in \mathrm{Ring}\to 0_{\mathrm{I}\left(R\right)}=0_R$$
16	3 15	eqtr4id	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}=0_{\mathrm{I}\left(R\right)}$$
17	16	oveq1d	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}{\cdot }_P{1}_P=0_{\mathrm{I}\left(R\right)}{\cdot }_P{1}_P$$
18	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
19	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
20		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
21	20 11	ringidcl	$$⊢P\in \mathrm{Ring}\to 1_P\in {\mathrm{Base}}_P$$
22	19 21	syl	$$⊢R\in \mathrm{Ring}\to 1_P\in {\mathrm{Base}}_P$$
23		eqid	$$⊢0_{\mathrm{I}\left(R\right)}=0_{\mathrm{I}\left(R\right)}$$
24	20 7 10 23 4	lmod0vs	$$⊢\left(P\in \mathrm{LMod}\wedge 1_P\in {\mathrm{Base}}_P\right)\to 0_{\mathrm{I}\left(R\right)}{\cdot }_P{1}_P=Y$$
25	18 22 24	syl2anc	$$⊢R\in \mathrm{Ring}\to 0_{\mathrm{I}\left(R\right)}{\cdot }_P{1}_P=Y$$
26	13 17 25	3eqtrd	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=Y$$