gsummulgz

Description: Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsummulg.b	$⊢ B = {Base}_{G}$
	gsummulg.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	gsummulg.a	$⊢ φ \to A \in V$
	gsummulg.f	$⊢ (φ \land k \in A) \to X \in B$
	gsummulg.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
	gsummulgz.g	$⊢ φ \to G \in Abel$
	gsummulgz.n	$⊢ φ \to N \in ℤ$
Assertion	gsummulgz	$⊢ φ \to \underset{k \in A}{\sum_{G}} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} (\underset{k \in A}{\sum_{G}}, X)$

Step	Hyp	Ref	Expression
1		gsummulg.b	$⊢ B = {Base}_{G}$
2		gsummulg.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		gsummulg.a	$⊢ φ \to A \in V$
5		gsummulg.f	$⊢ (φ \land k \in A) \to X \in B$
6		gsummulg.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((k \in A ⟼ X))$
7		gsummulgz.g	$⊢ φ \to G \in Abel$
8		gsummulgz.n	$⊢ φ \to N \in ℤ$
9		ablcmn	$⊢ G \in Abel \to G \in CMnd$
10	7 9	syl	$⊢ φ \to G \in CMnd$
11	7	orcd	$⊢ φ \to (G \in Abel \lor N \in ℕ_{0})$
12	1 2 3 4 5 6 10 8 11	gsummulglem	$⊢ φ \to \underset{k \in A}{\sum_{G}} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} (\underset{k \in A}{\sum_{G}}, X)$

Metamath Proof Explorer