Theorem gsummoncoe1fz

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. See gsummoncoe1fzo . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummoncoe1fz.1	|- P = ( Poly1 ` R )
	gsummoncoe1fz.2	|- B = ( Base ` P )
	gsummoncoe1fz.3	|- X = ( var1 ` R )
	gsummoncoe1fz.4	|- .^ = ( .g ` ( mulGrp ` P ) )
	gsummoncoe1fz.5	|- ( ph -> R e. Ring )
	gsummoncoe1fz.6	|- K = ( Base ` R )
	gsummoncoe1fz.7	|- .* = ( .s ` P )
	gsummoncoe1fz.8	|- ( ph -> D e. NN0 )
	gsummoncoe1fz.9	|- ( ph -> A. k e. ( 0 ... D ) A e. K )
	gsummoncoe1fz.10	|- ( ph -> L e. ( 0 ... D ) )
	gsummoncoe1fz.11	|- ( k = L -> A = C )
Assertion	gsummoncoe1fz	|- ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = C )

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fz.1	|- P = ( Poly1 ` R )
2		gsummoncoe1fz.2	|- B = ( Base ` P )
3		gsummoncoe1fz.3	|- X = ( var1 ` R )
4		gsummoncoe1fz.4	|- .^ = ( .g ` ( mulGrp ` P ) )
5		gsummoncoe1fz.5	|- ( ph -> R e. Ring )
6		gsummoncoe1fz.6	|- K = ( Base ` R )
7		gsummoncoe1fz.7	|- .* = ( .s ` P )
8		gsummoncoe1fz.8	|- ( ph -> D e. NN0 )
9		gsummoncoe1fz.9	|- ( ph -> A. k e. ( 0 ... D ) A e. K )
10		gsummoncoe1fz.10	|- ( ph -> L e. ( 0 ... D ) )
11		gsummoncoe1fz.11	|- ( k = L -> A = C )
12	8	nn0zd	|- ( ph -> D e. ZZ )
13		fzval3	|- ( D e. ZZ -> ( 0 ... D ) = ( 0 ..^ ( D + 1 ) ) )
14	12 13	syl	|- ( ph -> ( 0 ... D ) = ( 0 ..^ ( D + 1 ) ) )
15	14	mpteq1d	|- ( ph -> ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) = ( k e. ( 0 ..^ ( D + 1 ) ) |-> ( A .* ( k .^ X ) ) ) )
16	15	oveq2d	|- ( ph -> ( P gsum ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ..^ ( D + 1 ) ) |-> ( A .* ( k .^ X ) ) ) ) )
17	16	fveq2d	|- ( ph -> ( coe1 ` ( P gsum ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) ) ) = ( coe1 ` ( P gsum ( k e. ( 0 ..^ ( D + 1 ) ) |-> ( A .* ( k .^ X ) ) ) ) ) )
18	17	fveq1d	|- ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ ( D + 1 ) ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) )
19		eqid	|- ( 0g ` R ) = ( 0g ` R )
20	9 14	raleqtrdv	|- ( ph -> A. k e. ( 0 ..^ ( D + 1 ) ) A e. K )
21	10 14	eleqtrd	|- ( ph -> L e. ( 0 ..^ ( D + 1 ) ) )
22		peano2nn0	|- ( D e. NN0 -> ( D + 1 ) e. NN0 )
23	8 22	syl	|- ( ph -> ( D + 1 ) e. NN0 )
24	1 2 3 4 5 6 7 19 20 21 23 11	gsummoncoe1fzo	|- ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ..^ ( D + 1 ) ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = C )
25	18 24	eqtrd	|- ( ph -> ( ( coe1 ` ( P gsum ( k e. ( 0 ... D ) |-> ( A .* ( k .^ X ) ) ) ) ) ` L ) = C )