Theorem evl1at0

Description: Polynomial evaluation for the 0 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)$$
	evl1at0.0	$$⊢\underset{\dot{}}{0}=0_R$$
	evl1at0.z	$$⊢Z=0_P$$
Assertion	evl1at0	$$⊢R\in \mathrm{CRing}\to O\left(Z\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$

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		evl1at0.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		evl1at0.z	$$⊢Z=0_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	ply1scl0	$$⊢R\in \mathrm{Ring}\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)=Z$$
8	5 7	syl	$$⊢R\in \mathrm{CRing}\to \mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)=Z$$
9	8	eqcomd	$$⊢R\in \mathrm{CRing}\to Z=\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)$$
10	9	fveq2d	$$⊢R\in \mathrm{CRing}\to O\left(Z\right)=O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)\right)$$
11	10	fveq1d	$$⊢R\in \mathrm{CRing}\to O\left(Z\right)\left(\underset{\dot{}}{0}\right)=O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)\right)\left(\underset{\dot{}}{0}\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		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
16	12 3	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
17	5 15 16	3syl	$$⊢R\in \mathrm{CRing}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
18	1 2 12 6 13 14 17 17	evl1scad	$$⊢R\in \mathrm{CRing}\to \left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_P\wedge O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\right)$$
19	18	simprd	$$⊢R\in \mathrm{CRing}\to O\left(\mathrm{algSc}\left(P\right)\left(\underset{\dot{}}{0}\right)\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
20	11 19	eqtrd	$$⊢R\in \mathrm{CRing}\to O\left(Z\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$