Metamath Proof Explorer

Theorem gsumsmonply1

Description: A finite group sum of scaled monomials is a univariate polynomial. (Contributed by AV, 8-Oct-2019)

Ref Expression
Hypotheses gsummonply1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
gsummonply1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
gsummonply1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
gsummonply1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
gsummonply1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummonply1.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
gsummonply1.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
gsummonply1.0 ⊢ 0 = ( 0g ‘ 𝑅 )
gsummonply1.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
gsummonply1.f ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
Assertion gsumsmonply1 ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsummonply1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 gsummonply1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 gsummonply1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
4 gsummonply1.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
5 gsummonply1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummonply1.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
7 gsummonply1.m ⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
8 gsummonply1.0 ⊢ 0 = ( 0g ‘ 𝑅 )
9 gsummonply1.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
10 gsummonply1.f ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
11 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
12 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13 ringcmn ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
14 5 12 13 3syl ⊢ ( 𝜑 → 𝑃 ∈ CMnd )
15 nn0ex ⊢ ℕ0 ∈ V
16 15 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
17 9 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 )
18 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑅 ∈ Ring )
19 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
20 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑘 ∈ ℕ0 )
21 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
22 6 1 3 7 21 4 2 ply1tmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
23 18 19 20 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
24 17 23 mpd3an3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
25 24 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐵 )
26 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
27 5 26 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
28 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
29 5 28 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
30 1 3 21 4 2 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
31 5 30 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
32 16 27 29 2 17 31 11 8 7 10 mptscmfsupp0 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
33 2 11 14 16 25 32 gsumcl ⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐵 )