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

Metamath Proof Explorer

Theorem gsummoncoe1fzo

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses gsummoncoe1fzo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
gsummoncoe1fzo.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
gsummoncoe1fzo.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
gsummoncoe1fzo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
gsummoncoe1fzo.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummoncoe1fzo.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
gsummoncoe1fzo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
gsummoncoe1fzo.1 ⊢ 0 = ( 0g ‘ 𝑅 )
gsummoncoe1fzo.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝐴 ∈ 𝐾 )
gsummoncoe1fzo.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ 𝑁 ) )
gsummoncoe1fzo.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummoncoe1fzo.2 ⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
Assertion gsummoncoe1fzo ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 gsummoncoe1fzo.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 gsummoncoe1fzo.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 gsummoncoe1fzo.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
4 gsummoncoe1fzo.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
5 gsummoncoe1fzo.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummoncoe1fzo.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
7 gsummoncoe1fzo.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
8 gsummoncoe1fzo.1 ⊢ 0 = ( 0g ‘ 𝑅 )
9 gsummoncoe1fzo.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝐴 ∈ 𝐾 )
10 gsummoncoe1fzo.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ 𝑁 ) )
11 gsummoncoe1fzo.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 gsummoncoe1fzo.2 ⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
13 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
14 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 5 14 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
16 15 ringcmnd ⊢ ( 𝜑 → 𝑃 ∈ CMnd )
17 nn0ex ⊢ ℕ0 ∈ V
18 17 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) )
20 19 eldifbd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) )
21 20 iffalsed ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = 0 )
22 21 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) )
23 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑅 ∈ Ring )
24 19 eldifad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
25 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
26 25 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
27 25 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
28 15 27 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
31 3 1 2 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
32 5 31 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
34 26 4 29 30 33 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
35 24 34 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
36 1 2 7 8 ply10s0 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
37 23 35 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
38 22 37 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
39 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
40 39 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
41 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
42 5 41 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
44 9 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐾 )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐾 )
46 6 8 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
47 5 46 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ 𝐾 )
49 45 48 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ 𝐾 )
50 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
51 5 50 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
52 51 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
53 6 52 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
55 49 54 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
56 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
57 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
58 2 56 7 57 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
59 43 55 34 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
60 fzo0ssnn0 ⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
61 60 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ℕ0 )
62 2 13 16 18 38 40 59 61 gsummptres2 ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
63 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ..^ 𝑁 ) )
64 63 iftrued ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = 𝐴 )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
67 66 oveq2d ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
68 62 67 eqtrd ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
69 68 fveq2d ⊢ ( 𝜑 → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
70 69 fveq1d ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) )
71 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ 𝐾 )
72 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
73 72 18 40 44 47 mptiffisupp ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ) finSupp 0 )
74 60 10 sselid ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
75 1 2 3 4 5 6 7 8 71 73 74 gsummoncoe1 ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
76 70 75 eqtr3d ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
77 eleq1 ⊢ ( 𝑘 = 𝐿 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐿 ∈ ( 0 ..^ 𝑁 ) ) )
78 77 12 ifbieq1d ⊢ ( 𝑘 = 𝐿 → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑘 = 𝐿 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
80 10 79 csbied ⊢ ( 𝜑 → ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
81 10 iftrued ⊢ ( 𝜑 → if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) = 𝐶 )
82 76 80 81 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )