Theorem evl1at0

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

	Ref	Expression
Hypotheses	evl1at0.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1at0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1at0.0	⊢ 0 = ( 0g ‘ 𝑅 )
	evl1at0.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
Assertion	evl1at0	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝑍 ) ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		evl1at0.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1at0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		evl1at0.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		evl1at0.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
5		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
7	2 6 3 4	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ 0 ) = 𝑍 )
8	5 7	syl	⊢ ( 𝑅 ∈ CRing → ( ( algSc ‘ 𝑃 ) ‘ 0 ) = 𝑍 )
9	8	eqcomd	⊢ ( 𝑅 ∈ CRing → 𝑍 = ( ( algSc ‘ 𝑃 ) ‘ 0 ) )
10	9	fveq2d	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑍 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 0 ) ) )
11	10	fveq1d	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝑍 ) ‘ 0 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 0 ) ) ‘ 0 ) )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14		id	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
15		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
16	12 3	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
17	5 15 16	3syl	⊢ ( 𝑅 ∈ CRing → 0 ∈ ( Base ‘ 𝑅 ) )
18	1 2 12 6 13 14 17 17	evl1scad	⊢ ( 𝑅 ∈ CRing → ( ( ( algSc ‘ 𝑃 ) ‘ 0 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 0 ) ) ‘ 0 ) = 0 ) )
19	18	simprd	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 0 ) ) ‘ 0 ) = 0 )
20	11 19	eqtrd	⊢ ( 𝑅 ∈ CRing → ( ( 𝑂 ‘ 𝑍 ) ‘ 0 ) = 0 )