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 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐵 )