Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	ply1scl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1scl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	ply1scl1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	ply1scl1.n	$$⊢N=1_P$$
Assertion	ply1scl1	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=N$$

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		ply1scl1.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		ply1scl1.n	$$⊢N=1_P$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
7	1	ply1sca2	$$⊢\mathrm{I}\left(R\right)=\mathrm{Scalar}\left(P\right)$$
8		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
9	8 5	strfvi	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{I}\left(R\right)}$$
10		eqid	$$⊢{\cdot }_P={\cdot }_P$$
11	2 7 9 10 4	asclval	$$⊢\underset{\dot{}}{1}\in {\mathrm{Base}}_R\to A\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}{\cdot }_{P}N$$
12	6 11	syl	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}{\cdot }_{P}N$$
13		fvi	$$⊢R\in \mathrm{Ring}\to \mathrm{I}\left(R\right)=R$$
14	13	fveq2d	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{I}\left(R\right)}=1_R$$
15	14 3	eqtr4di	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{I}\left(R\right)}=\underset{\dot{}}{1}$$
16	15	oveq1d	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{I}\left(R\right)}{\cdot }_{P}N=\underset{\dot{}}{1}{\cdot }_{P}N$$
17	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
18	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
19		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
20	19 4	ringidcl	$$⊢P\in \mathrm{Ring}\to N\in {\mathrm{Base}}_P$$
21	18 20	syl	$$⊢R\in \mathrm{Ring}\to N\in {\mathrm{Base}}_P$$
22		eqid	$$⊢1_{\mathrm{I}\left(R\right)}=1_{\mathrm{I}\left(R\right)}$$
23	19 7 10 22	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge N\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{I}\left(R\right)}{\cdot }_{P}N=N$$
24	17 21 23	syl2anc	$$⊢R\in \mathrm{Ring}\to 1_{\mathrm{I}\left(R\right)}{\cdot }_{P}N=N$$
25	12 16 24	3eqtr2d	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=N$$