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={\mathrm{Poly}}_1\left(R\right)$$
	gsummoncoe1fz.2	$$⊢B={\mathrm{Base}}_P$$
	gsummoncoe1fz.3	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	gsummoncoe1fz.4	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	gsummoncoe1fz.5	$$⊢\phi \to R\in \mathrm{Ring}$$
	gsummoncoe1fz.6	$$⊢K={\mathrm{Base}}_R$$
	gsummoncoe1fz.7	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
	gsummoncoe1fz.8	$$⊢\phi \to D\in {\mathbb{N}}_0$$
	gsummoncoe1fz.9	$$⊢\phi \to \forall k\in \left(0\dots D\right)A\in K$$
	gsummoncoe1fz.10	$$⊢\phi \to L\in \left(0\dots D\right)$$
	gsummoncoe1fz.11	$$⊢k=L\to A=C$$
Assertion	gsummoncoe1fz	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k=0}{\overset{D}{{\sum }_P}}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fz.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		gsummoncoe1fz.2	$$⊢B={\mathrm{Base}}_P$$
3		gsummoncoe1fz.3	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		gsummoncoe1fz.4	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
5		gsummoncoe1fz.5	$$⊢\phi \to R\in \mathrm{Ring}$$
6		gsummoncoe1fz.6	$$⊢K={\mathrm{Base}}_R$$
7		gsummoncoe1fz.7	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
8		gsummoncoe1fz.8	$$⊢\phi \to D\in {\mathbb{N}}_0$$
9		gsummoncoe1fz.9	$$⊢\phi \to \forall k\in \left(0\dots D\right)A\in K$$
10		gsummoncoe1fz.10	$$⊢\phi \to L\in \left(0\dots D\right)$$
11		gsummoncoe1fz.11	$$⊢k=L\to A=C$$
12	8	nn0zd	$$⊢\phi \to D\in \mathbb{Z}$$
13		fzval3	$$⊢D\in \mathbb{Z}\to \left(0\dots D\right)=\left(0..^D+1\right)$$
14	12 13	syl	$$⊢\phi \to \left(0\dots D\right)=\left(0..^D+1\right)$$
15	14	mpteq1d	$$⊢\phi \to \left(k\in \left(0\dots D\right)⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(k\in \left(0..^D+1\right)⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
16	15	oveq2d	$$⊢\phi \to \underset{k=0}{\overset{D}{{\sum }_P}}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{k\in \left(0..^D+1\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k=0}{\overset{D}{{\sum }_P}}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)={\mathrm{coe}}_1\left(\underset{k\in \left(0..^D+1\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)$$
18	17	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k=0}{\overset{D}{{\sum }_P}}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)={\mathrm{coe}}_1\left(\underset{k\in \left(0..^D+1\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)$$
19		eqid	$$⊢0_R=0_R$$
20	9 14	raleqtrdv	$$⊢\phi \to \forall k\in \left(0..^D+1\right)A\in K$$
21	10 14	eleqtrd	$$⊢\phi \to L\in \left(0..^D+1\right)$$
22		peano2nn0	$$⊢D\in {\mathbb{N}}_0\to D+1\in {\mathbb{N}}_0$$
23	8 22	syl	$$⊢\phi \to D+1\in {\mathbb{N}}_0$$
24	1 2 3 4 5 6 7 19 20 21 23 11	gsummoncoe1fzo	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in \left(0..^D+1\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=C$$
25	18 24	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k=0}{\overset{D}{{\sum }_P}}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=C$$