Theorem evl1at0

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

	Ref	Expression
Hypotheses	evl1at0.o	|- O = ( eval1 ` R )
	evl1at0.p	|- P = ( Poly1 ` R )
	evl1at0.0	|- .0. = ( 0g ` R )
	evl1at0.z	|- Z = ( 0g ` P )
Assertion	evl1at0	|- ( R e. CRing -> ( ( O ` Z ) ` .0. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		evl1at0.o	|- O = ( eval1 ` R )
2		evl1at0.p	|- P = ( Poly1 ` R )
3		evl1at0.0	|- .0. = ( 0g ` R )
4		evl1at0.z	|- Z = ( 0g ` P )
5		crngring	|- ( R e. CRing -> R e. Ring )
6		eqid	|- ( algSc ` P ) = ( algSc ` P )
7	2 6 3 4	ply1scl0	|- ( R e. Ring -> ( ( algSc ` P ) ` .0. ) = Z )
8	5 7	syl	|- ( R e. CRing -> ( ( algSc ` P ) ` .0. ) = Z )
9	8	eqcomd	|- ( R e. CRing -> Z = ( ( algSc ` P ) ` .0. ) )
10	9	fveq2d	|- ( R e. CRing -> ( O ` Z ) = ( O ` ( ( algSc ` P ) ` .0. ) ) )
11	10	fveq1d	|- ( R e. CRing -> ( ( O ` Z ) ` .0. ) = ( ( O ` ( ( algSc ` P ) ` .0. ) ) ` .0. ) )
12		eqid	|- ( Base ` R ) = ( Base ` R )
13		eqid	|- ( Base ` P ) = ( Base ` P )
14		id	|- ( R e. CRing -> R e. CRing )
15		ringgrp	|- ( R e. Ring -> R e. Grp )
16	12 3	grpidcl	|- ( R e. Grp -> .0. e. ( Base ` R ) )
17	5 15 16	3syl	|- ( R e. CRing -> .0. e. ( Base ` R ) )
18	1 2 12 6 13 14 17 17	evl1scad	|- ( R e. CRing -> ( ( ( algSc ` P ) ` .0. ) e. ( Base ` P ) /\ ( ( O ` ( ( algSc ` P ) ` .0. ) ) ` .0. ) = .0. ) )
19	18	simprd	|- ( R e. CRing -> ( ( O ` ( ( algSc ` P ) ` .0. ) ) ` .0. ) = .0. )
20	11 19	eqtrd	|- ( R e. CRing -> ( ( O ` Z ) ` .0. ) = .0. )