evl1at1

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

	Ref	Expression
Hypotheses	evl1at0.o	$⊢ O = {eval}_{1} (R)$
	evl1at0.p	$⊢ P = {Poly}_{1} (R)$
	evl1at1.1	$⊢ \underset{˙}{1} = 1_{R}$
	evl1at1.i	$⊢ I = 1_{P}$
Assertion	evl1at1	$⊢ R \in CRing \to O (I) (\underset{˙}{1}) = \underset{˙}{1}$

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

Metamath Proof Explorer