Theorem evl1at1

Description: Polynomial evaluation for the 1 scalar. (Contributed by AV, 10-Aug-2019)

	Ref	Expression
Hypotheses	evl1at0.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	evl1at0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	evl1at1.1	$$⊢\underset{\dot{}}{1}=1_R$$
	evl1at1.i	$$⊢I=1_P$$
Assertion	evl1at1	$$⊢R\in \mathrm{CRing}\to O\left(I\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		evl1at0.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
2		evl1at0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		evl1at1.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		evl1at1.i	$$⊢I=1_P$$
5		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
6		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
7	2 6 3 4	ply1scl1	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)=I$$
8	5 7	syl	$$⊢R\in \mathrm{CRing}\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)=I$$
9	8	eqcomd	$$⊢R\in \mathrm{CRing}\to I=\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)$$
10	9	fveq2d	$$⊢R\in \mathrm{CRing}\to O\left(I\right)=O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)$$
11	10	fveq1d	$$⊢R\in \mathrm{CRing}\to O\left(I\right)\left(\underset{\dot{}}{1}\right)=O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)\left(\underset{\dot{}}{1}\right)$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
14		id	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{CRing}$$
15	12 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
16	5 15	syl	$$⊢R\in \mathrm{CRing}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
17	1 2 12 6 13 14 16 16	evl1scad	$$⊢R\in \mathrm{CRing}\to \left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_P\wedge O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}\right)$$
18	17	simprd	$$⊢R\in \mathrm{CRing}\to O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{1}\right)\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
19	11 18	eqtrd	$$⊢R\in \mathrm{CRing}\to O\left(I\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$