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	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	gsummonply1.b	$$⊢B={\mathrm{Base}}_P$$
	gsummonply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	gsummonply1.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	gsummonply1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	gsummonply1.k	$$⊢K={\mathrm{Base}}_R$$
	gsummonply1.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
	gsummonply1.0	$$⊢\underset{\dot{}}{0}=0_R$$
	gsummonply1.a	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in K$$
	gsummonply1.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼A\right)\right)$$
Assertion	gsumsmonply1	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		gsummonply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		gsummonply1.b	$$⊢B={\mathrm{Base}}_P$$
3		gsummonply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		gsummonply1.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
5		gsummonply1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		gsummonply1.k	$$⊢K={\mathrm{Base}}_R$$
7		gsummonply1.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
8		gsummonply1.0	$$⊢\underset{\dot{}}{0}=0_R$$
9		gsummonply1.a	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in K$$
10		gsummonply1.f	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼A\right)\right)$$
11		eqid	$$⊢0_P=0_P$$
12	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
13		ringcmn	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{CMnd}$$
14	5 12 13	3syl	$$⊢\phi \to P\in \mathrm{CMnd}$$
15		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
17	9	r19.21bi	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\in K$$
18	5	3ad2ant1	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\wedge A\in K\right)\to R\in \mathrm{Ring}$$
19		simp3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\wedge A\in K\right)\to A\in K$$
20		simp2	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\wedge A\in K\right)\to k\in {\mathbb{N}}_0$$
21		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
22	6 1 3 7 21 4 2	ply1tmcl	$$⊢\left(R\in \mathrm{Ring}\wedge A\in K\wedge k\in {\mathbb{N}}_0\right)\to A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\in B$$
23	18 19 20 22	syl3anc	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\wedge A\in K\right)\to A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\in B$$
24	17 23	mpd3an3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\in B$$
25	24	fmpttd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right):{\mathbb{N}}_0⟶B$$
26	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
27	5 26	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
28	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
29	5 28	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
30	1 3 21 4 2	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge k\in {\mathbb{N}}_0\right)\to k\underset{\dot{}}{\times }X\in B$$
31	5 30	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\underset{\dot{}}{\times }X\in B$$
32	16 27 29 2 17 31 11 8 7 10	mptscmfsupp0	$$⊢\phi \to {finSupp}_{0_P}\left(\left(k\in {\mathbb{N}}_0⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)$$
33	2 11 14 16 25 32	gsumcl	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\in B$$