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 = {Poly}_{1} (R)$
	gsummoncoe1fz.2	$⊢ B = {Base}_{P}$
	gsummoncoe1fz.3	$⊢ X = {var}_{1} (R)$
	gsummoncoe1fz.4	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	gsummoncoe1fz.5	$⊢ φ \to R \in Ring$
	gsummoncoe1fz.6	$⊢ K = {Base}_{R}$
	gsummoncoe1fz.7	$⊢ \underset{˙}{*} = \cdot_{P}$
	gsummoncoe1fz.8	$⊢ φ \to D \in ℕ_{0}$
	gsummoncoe1fz.9	$⊢ φ \to \forall k \in (0 \dots D) A \in K$
	gsummoncoe1fz.10	$⊢ φ \to L \in (0 \dots D)$
	gsummoncoe1fz.11	$⊢ k = L \to A = C$
Assertion	gsummoncoe1fz	$⊢ φ \to {coe}_{1} ({\sum_{P}}_{k = 0}^{D} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = C$

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fz.1	$⊢ P = {Poly}_{1} (R)$
2		gsummoncoe1fz.2	$⊢ B = {Base}_{P}$
3		gsummoncoe1fz.3	$⊢ X = {var}_{1} (R)$
4		gsummoncoe1fz.4	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
5		gsummoncoe1fz.5	$⊢ φ \to R \in Ring$
6		gsummoncoe1fz.6	$⊢ K = {Base}_{R}$
7		gsummoncoe1fz.7	$⊢ \underset{˙}{*} = \cdot_{P}$
8		gsummoncoe1fz.8	$⊢ φ \to D \in ℕ_{0}$
9		gsummoncoe1fz.9	$⊢ φ \to \forall k \in (0 \dots D) A \in K$
10		gsummoncoe1fz.10	$⊢ φ \to L \in (0 \dots D)$
11		gsummoncoe1fz.11	$⊢ k = L \to A = C$
12	8	nn0zd	$⊢ φ \to D \in ℤ$
13		fzval3	$⊢ D \in ℤ \to (0 \dots D) = (0 ..^D + 1)$
14	12 13	syl	$⊢ φ \to (0 \dots D) = (0 ..^D + 1)$
15	14	mpteq1d	$⊢ φ \to (k \in (0 \dots D) ⟼ A \underset{˙}{} (k \underset{˙}{\times} X)) = (k \in (0 ..^D + 1) ⟼ A \underset{˙}{} (k \underset{˙}{\times} X))$
16	15	oveq2d	$⊢ φ \to {\sum_{P}}_{k = 0}^{D} (A \underset{˙}{} (k \underset{˙}{\times} X)) = \underset{k \in (0 ..^D + 1)}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X))$
17	16	fveq2d	$⊢ φ \to {coe}_{1} ({\sum_{P}}_{k = 0}^{D} (A \underset{˙}{} (k \underset{˙}{\times} X))) = {coe}_{1} (\underset{k \in (0 ..^D + 1)}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X)))$
18	17	fveq1d	$⊢ φ \to {coe}_{1} ({\sum_{P}}_{k = 0}^{D} (A \underset{˙}{} (k \underset{˙}{\times} X))) (L) = {coe}_{1} (\underset{k \in (0 ..^D + 1)}{\sum_{P}} (A \underset{˙}{} (k \underset{˙}{\times} X))) (L)$
19		eqid	$⊢ 0_{R} = 0_{R}$
20	9 14	raleqtrdv	$⊢ φ \to \forall k \in (0 ..^D + 1) A \in K$
21	10 14	eleqtrd	$⊢ φ \to L \in (0 ..^D + 1)$
22		peano2nn0	$⊢ D \in ℕ_{0} \to D + 1 \in ℕ_{0}$
23	8 22	syl	$⊢ φ \to D + 1 \in ℕ_{0}$
24	1 2 3 4 5 6 7 19 20 21 23 11	gsummoncoe1fzo	$⊢ φ \to {coe}_{1} (\underset{k \in (0 ..^D + 1)}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = C$
25	18 24	eqtrd	$⊢ φ \to {coe}_{1} ({\sum_{P}}_{k = 0}^{D} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = C$

Metamath Proof Explorer

Theorem gsummoncoe1fz

Proof