Theorem evl1at1

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

	Ref	Expression
Hypotheses	evl1at0.o	|- O = ( eval1 ` R )
	evl1at0.p	|- P = ( Poly1 ` R )
	evl1at1.1	|- .1. = ( 1r ` R )
	evl1at1.i	|- I = ( 1r ` P )
Assertion	evl1at1	|- ( R e. CRing -> ( ( O ` I ) ` .1. ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		evl1at0.o	|- O = ( eval1 ` R )
2		evl1at0.p	|- P = ( Poly1 ` R )
3		evl1at1.1	|- .1. = ( 1r ` R )
4		evl1at1.i	|- I = ( 1r ` P )
5		crngring	|- ( R e. CRing -> R e. Ring )
6		eqid	|- ( algSc ` P ) = ( algSc ` P )
7	2 6 3 4	ply1scl1	|- ( R e. Ring -> ( ( algSc ` P ) ` .1. ) = I )
8	5 7	syl	|- ( R e. CRing -> ( ( algSc ` P ) ` .1. ) = I )
9	8	eqcomd	|- ( R e. CRing -> I = ( ( algSc ` P ) ` .1. ) )
10	9	fveq2d	|- ( R e. CRing -> ( O ` I ) = ( O ` ( ( algSc ` P ) ` .1. ) ) )
11	10	fveq1d	|- ( R e. CRing -> ( ( O ` I ) ` .1. ) = ( ( O ` ( ( algSc ` P ) ` .1. ) ) ` .1. ) )
12		eqid	|- ( Base ` R ) = ( Base ` R )
13		eqid	|- ( Base ` P ) = ( Base ` P )
14		id	|- ( R e. CRing -> R e. CRing )
15	12 3	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
16	5 15	syl	|- ( R e. CRing -> .1. e. ( Base ` R ) )
17	1 2 12 6 13 14 16 16	evl1scad	|- ( R e. CRing -> ( ( ( algSc ` P ) ` .1. ) e. ( Base ` P ) /\ ( ( O ` ( ( algSc ` P ) ` .1. ) ) ` .1. ) = .1. ) )
18	17	simprd	|- ( R e. CRing -> ( ( O ` ( ( algSc ` P ) ` .1. ) ) ` .1. ) = .1. )
19	11 18	eqtrd	|- ( R e. CRing -> ( ( O ` I ) ` .1. ) = .1. )