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 = {Poly}_{1} (R)$
	gsummonply1.b	$⊢ B = {Base}_{P}$
	gsummonply1.x	$⊢ X = {var}_{1} (R)$
	gsummonply1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	gsummonply1.r	$⊢ φ \to R \in Ring$
	gsummonply1.k	$⊢ K = {Base}_{R}$
	gsummonply1.m	$⊢ \underset{˙}{*} = \cdot_{P}$
	gsummonply1.0	$⊢ \underset{˙}{0} = 0_{R}$
	gsummonply1.a	$⊢ φ \to \forall k \in ℕ_{0} A \in K$
	gsummonply1.f	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ A))$
Assertion	gsumsmonply1	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X)) \in B$

Proof

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

Metamath Proof Explorer

Theorem gsumsmonply1

Proof