Theorem ply1ascl1

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

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

Proof

Step	Hyp	Ref	Expression
1		ply1ascl1.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
2		ply1ascl1.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
3		ply1ascl1.i	$$⊢I=1_R$$
4		ply1ascl1.1	$$⊢\underset{\dot{}}{1}=1_W$$
5		ply1ascl1.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 1_R=1_{\mathrm{Scalar}\left(W\right)}$$
9	3 8	eqtrid	$$⊢\phi \to I=1_{\mathrm{Scalar}\left(W\right)}$$
10	9	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(I\right)=\mathrm{algSc}\left(W\right)\left(1_{\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	ascl1	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(1_{\mathrm{Scalar}\left(W\right)}\right)=1_W$$
18	10 17	eqtrd	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(I\right)=1_W$$
19	2	fveq1i	$$⊢A\left(I\right)=\mathrm{algSc}\left(W\right)\left(I\right)$$
20	18 19 4	3eqtr4g	$$⊢\phi \to A\left(I\right)=\underset{\dot{}}{1}$$