Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015) (Proof shortened by SN, 12-Mar-2025)

	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	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
6	5	fveq2d	$$⊢R\in \mathrm{Ring}\to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
7	3 6	eqtrid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(P\right)}$$
8	7	fveq2d	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=A\left(1_{\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	ascl1	$$⊢R\in \mathrm{Ring}\to A\left(1_{\mathrm{Scalar}\left(P\right)}\right)=1_P$$
13	8 12	eqtrd	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=1_P$$
14	13 4	eqtr4di	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=N$$