Theorem coe1tmfv1

Description: Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	coe1tm.z	|- .0. = ( 0g ` R )
	coe1tm.k	|- K = ( Base ` R )
	coe1tm.p	|- P = ( Poly1 ` R )
	coe1tm.x	|- X = ( var1 ` R )
	coe1tm.m	|- .x. = ( .s ` P )
	coe1tm.n	|- N = ( mulGrp ` P )
	coe1tm.e	|- .^ = ( .g ` N )
Assertion	coe1tmfv1	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	|- .0. = ( 0g ` R )
2		coe1tm.k	|- K = ( Base ` R )
3		coe1tm.p	|- P = ( Poly1 ` R )
4		coe1tm.x	|- X = ( var1 ` R )
5		coe1tm.m	|- .x. = ( .s ` P )
6		coe1tm.n	|- N = ( mulGrp ` P )
7		coe1tm.e	|- .^ = ( .g ` N )
8	1 2 3 4 5 6 7	coe1tm	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
9	8	fveq1d	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = ( ( x e. NN0 |-> if ( x = D , C , .0. ) ) ` D ) )
10		eqid	|- ( x e. NN0 |-> if ( x = D , C , .0. ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) )
11		iftrue	|- ( x = D -> if ( x = D , C , .0. ) = C )
12		simp3	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> D e. NN0 )
13		simp2	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> C e. K )
14	10 11 12 13	fvmptd3	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( x e. NN0 |-> if ( x = D , C , .0. ) ) ` D ) = C )
15	9 14	eqtrd	|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` D ) = C )