Theorem coe1id

Description: Coefficient vector of the unit polynomial. (Contributed by AV, 9-Aug-2019)

	Ref	Expression
Hypotheses	coe1id.p	|- P = ( Poly1 ` R )
	coe1id.i	|- I = ( 1r ` P )
	coe1id.0	|- .0. = ( 0g ` R )
	coe1id.1	|- .1. = ( 1r ` R )
Assertion	coe1id	|- ( R e. Ring -> ( coe1 ` I ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1id.p	|- P = ( Poly1 ` R )
2		coe1id.i	|- I = ( 1r ` P )
3		coe1id.0	|- .0. = ( 0g ` R )
4		coe1id.1	|- .1. = ( 1r ` R )
5		eqid	|- ( algSc ` P ) = ( algSc ` P )
6	1 5 4 2	ply1scl1	|- ( R e. Ring -> ( ( algSc ` P ) ` .1. ) = I )
7	6	eqcomd	|- ( R e. Ring -> I = ( ( algSc ` P ) ` .1. ) )
8	7	fveq2d	|- ( R e. Ring -> ( coe1 ` I ) = ( coe1 ` ( ( algSc ` P ) ` .1. ) ) )
9		eqid	|- ( Base ` R ) = ( Base ` R )
10	9 4	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
11	1 5 9 3	coe1scl	|- ( ( R e. Ring /\ .1. e. ( Base ` R ) ) -> ( coe1 ` ( ( algSc ` P ) ` .1. ) ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )
12	10 11	mpdan	|- ( R e. Ring -> ( coe1 ` ( ( algSc ` P ) ` .1. ) ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )
13	8 12	eqtrd	|- ( R e. Ring -> ( coe1 ` I ) = ( x e. NN0 |-> if ( x = 0 , .1. , .0. ) ) )