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 )

Metamath Proof Explorer

Theorem gsummoncoe1fz

Proof