gsummulglem

	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))$
	gsummulglem.g	$⊢ φ \to G \in CMnd$
	gsummulglem.n	$⊢ φ \to N \in ℤ$
	gsummulglem.o	$⊢ φ \to (G \in Abel \lor N \in ℕ_{0})$
Assertion	gsummulglem	$⊢ φ \to \underset{k \in A}{\sum_{G}} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} (\underset{k \in A}{\sum_{G}}, X)$

Proof

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		gsummulglem.g	$⊢ φ \to G \in CMnd$
8		gsummulglem.n	$⊢ φ \to N \in ℤ$
9		gsummulglem.o	$⊢ φ \to (G \in Abel \lor N \in ℕ_{0})$
10		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
11	7 10	syl	$⊢ φ \to G \in Mnd$
12	1 3	mulgghm	$⊢ (G \in Abel \land N \in ℤ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G GrpHom G)$
13		ghmmhm	$⊢ (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G GrpHom G) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G)$
14	12 13	syl	$⊢ (G \in Abel \land N \in ℤ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G)$
15	14	expcom	$⊢ N \in ℤ \to (G \in Abel \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G))$
16	8 15	syl	$⊢ φ \to (G \in Abel \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G))$
17	1 3	mulgmhm	$⊢ (G \in CMnd \land N \in ℕ_{0}) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G)$
18	17	ex	$⊢ G \in CMnd \to (N \in ℕ_{0} \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G))$
19	7 18	syl	$⊢ φ \to (N \in ℕ_{0} \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G))$
20	16 19 9	mpjaod	$⊢ φ \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (G MndHom G)$
21		oveq2	$⊢ x = X \to N \underset{˙}{\cdot} x = N \underset{˙}{\cdot} X$
22		oveq2	$⊢ x = \underset{k \in A}{\sum_{G}} X \to N \underset{˙}{\cdot} x = N \underset{˙}{\cdot} (\underset{k \in A}{\sum_{G}}, X)$
23	1 2 7 11 4 20 5 6 21 22	gsummhm2	$⊢ φ \to \underset{k \in A}{\sum_{G}} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} (\underset{k \in A}{\sum_{G}}, X)$

Metamath Proof Explorer

Theorem gsummulglem

Proof