Theorem coe1scl

Description: Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	|- P = ( Poly1 ` R )
	ply1scl.a	|- A = ( algSc ` P )
	coe1scl.k	|- K = ( Base ` R )
	coe1scl.z	|- .0. = ( 0g ` R )
Assertion	coe1scl	|- ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	|- P = ( Poly1 ` R )
2		ply1scl.a	|- A = ( algSc ` P )
3		coe1scl.k	|- K = ( Base ` R )
4		coe1scl.z	|- .0. = ( 0g ` R )
5		eqid	|- ( var1 ` R ) = ( var1 ` R )
6		eqid	|- ( .s ` P ) = ( .s ` P )
7		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
8		eqid	|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
9	3 1 5 6 7 8 2	ply1scltm	|- ( ( R e. Ring /\ X e. K ) -> ( A ` X ) = ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
10	9	fveq2d	|- ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
11		0nn0	|- 0 e. NN0
12	4 3 1 5 6 7 8	coe1tm	|- ( ( R e. Ring /\ X e. K /\ 0 e. NN0 ) -> ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
13	11 12	mp3an3	|- ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )
14	10 13	eqtrd	|- ( ( R e. Ring /\ X e. K ) -> ( coe1 ` ( A ` X ) ) = ( x e. NN0 |-> if ( x = 0 , X , .0. ) ) )