Theorem coe1vr1

Description: Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	coe1vr1.1	|- P = ( Poly1 ` R )
	coe1vr1.2	|- X = ( var1 ` R )
	coe1vr1.3	|- ( ph -> R e. Ring )
	coe1vr1.4	|- .0. = ( 0g ` R )
	coe1vr1.5	|- .1. = ( 1r ` R )
Assertion	coe1vr1	|- ( ph -> ( coe1 ` X ) = ( k e. NN0 |-> if ( k = 1 , .1. , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1vr1.1	|- P = ( Poly1 ` R )
2		coe1vr1.2	|- X = ( var1 ` R )
3		coe1vr1.3	|- ( ph -> R e. Ring )
4		coe1vr1.4	|- .0. = ( 0g ` R )
5		coe1vr1.5	|- .1. = ( 1r ` R )
6		eqid	|- ( Base ` P ) = ( Base ` P )
7	2 1 6	vr1cl	|- ( R e. Ring -> X e. ( Base ` P ) )
8		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
9	8 6	mgpbas	|- ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
10		eqid	|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
11	9 10	mulg1	|- ( X e. ( Base ` P ) -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
12	3 7 11	3syl	|- ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) X ) = X )
13	12	fveq2d	|- ( ph -> ( coe1 ` ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( coe1 ` X ) )
14		1nn0	|- 1 e. NN0
15	14	a1i	|- ( ph -> 1 e. NN0 )
16	1 2 10 3 15 4 5	coe1mon	|- ( ph -> ( coe1 ` ( 1 ( .g ` ( mulGrp ` P ) ) X ) ) = ( k e. NN0 |-> if ( k = 1 , .1. , .0. ) ) )
17	13 16	eqtr3d	|- ( ph -> ( coe1 ` X ) = ( k e. NN0 |-> if ( k = 1 , .1. , .0. ) ) )