Theorem evl1at1

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

	Ref	Expression
Hypotheses	evl1at0.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1at0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1at1.1	⊢ 1 = ( 1r ‘ 𝑅 )
	evl1at1.i	⊢ 𝐼 = ( 1r ‘ 𝑃 )
Assertion	evl1at1	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝐼 ) ‘ 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		evl1at0.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1at0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		evl1at1.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		evl1at1.i	⊢ 𝐼 = ( 1r ‘ 𝑃 )
5		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
7	2 6 3 4	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ 1 ) = 𝐼 )
8	5 7	syl	⊢ ( 𝑅 ∈ CRing → ( ( algSc ‘ 𝑃 ) ‘ 1 ) = 𝐼 )
9	8	eqcomd	⊢ ( 𝑅 ∈ CRing → 𝐼 = ( ( algSc ‘ 𝑃 ) ‘ 1 ) )
10	9	fveq2d	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝐼 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) )
11	10	fveq1d	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝐼 ) ‘ 1 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) ‘ 1 ) )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14		id	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
15	12 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
16	5 15	syl	⊢ ( 𝑅 ∈ CRing → 1 ∈ ( Base ‘ 𝑅 ) )
17	1 2 12 6 13 14 16 16	evl1scad	⊢ ( 𝑅 ∈ CRing → ( ( ( algSc ‘ 𝑃 ) ‘ 1 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) ‘ 1 ) = 1 ) )
18	17	simprd	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 1 ) ) ‘ 1 ) = 1 )
19	11 18	eqtrd	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝐼 ) ‘ 1 ) = 1 )