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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	gsummoncoe1fz.2	⊢ 𝐵 = ( Base ‘ 𝑃 )
	gsummoncoe1fz.3	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	gsummoncoe1fz.4	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	gsummoncoe1fz.5	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	gsummoncoe1fz.6	⊢ 𝐾 = ( Base ‘ 𝑅 )
	gsummoncoe1fz.7	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
	gsummoncoe1fz.8	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
	gsummoncoe1fz.9	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝐷 ) 𝐴 ∈ 𝐾 )
	gsummoncoe1fz.10	⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... 𝐷 ) )
	gsummoncoe1fz.11	⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
Assertion	gsummoncoe1fz	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fz.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		gsummoncoe1fz.2	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		gsummoncoe1fz.3	⊢ 𝑋 = ( var1 ‘ 𝑅 )
4		gsummoncoe1fz.4	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
5		gsummoncoe1fz.5	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		gsummoncoe1fz.6	⊢ 𝐾 = ( Base ‘ 𝑅 )
7		gsummoncoe1fz.7	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
8		gsummoncoe1fz.8	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
9		gsummoncoe1fz.9	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝐷 ) 𝐴 ∈ 𝐾 )
10		gsummoncoe1fz.10	⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... 𝐷 ) )
11		gsummoncoe1fz.11	⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
12	8	nn0zd	⊢ ( 𝜑 → 𝐷 ∈ ℤ )
13		fzval3	⊢ ( 𝐷 ∈ ℤ → ( 0 ... 𝐷 ) = ( 0 ..^ ( 𝐷 + 1 ) ) )
14	12 13	syl	⊢ ( 𝜑 → ( 0 ... 𝐷 ) = ( 0 ..^ ( 𝐷 + 1 ) ) )
15	14	mpteq1d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
17	16	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) )
19		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20	9 14	raleqtrdv	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) 𝐴 ∈ 𝐾 )
21	10 14	eleqtrd	⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) )
22		peano2nn0	⊢ ( 𝐷 ∈ ℕ0 → ( 𝐷 + 1 ) ∈ ℕ0 )
23	8 22	syl	⊢ ( 𝜑 → ( 𝐷 + 1 ) ∈ ℕ0 )
24	1 2 3 4 5 6 7 19 20 21 23 11	gsummoncoe1fzo	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ ( 𝐷 + 1 ) ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )
25	18 24	eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )