This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ... 𝐷 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )