gsummptmhm

Description: Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018) (Revised by AV, 8-Sep-2019)

	Ref	Expression
Hypotheses	gsummptmhm.b	$⊢ B = {Base}_{G}$
	gsummptmhm.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptmhm.g	$⊢ φ \to G \in CMnd$
	gsummptmhm.h	$⊢ φ \to H \in Mnd$
	gsummptmhm.a	$⊢ φ \to A \in V$
	gsummptmhm.k	$⊢ φ \to K \in (G MndHom H)$
	gsummptmhm.c	$⊢ (φ \land x \in A) \to C \in B$
	gsummptmhm.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ C))$
Assertion	gsummptmhm	$⊢ φ \to \underset{x \in A}{\sum_{H}} K (C) = K (\underset{x \in A}{\sum_{G}} C)$

Proof

Step	Hyp	Ref	Expression
1		gsummptmhm.b	$⊢ B = {Base}_{G}$
2		gsummptmhm.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptmhm.g	$⊢ φ \to G \in CMnd$
4		gsummptmhm.h	$⊢ φ \to H \in Mnd$
5		gsummptmhm.a	$⊢ φ \to A \in V$
6		gsummptmhm.k	$⊢ φ \to K \in (G MndHom H)$
7		gsummptmhm.c	$⊢ (φ \land x \in A) \to C \in B$
8		gsummptmhm.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ C))$
9		eqidd	$⊢ φ \to (x \in A ⟼ C) = (x \in A ⟼ C)$
10		eqid	$⊢ {Base}_{H} = {Base}_{H}$
11	1 10	mhmf	$⊢ K \in (G MndHom H) \to K : B ⟶ {Base}_{H}$
12		ffn	$⊢ K : B ⟶ {Base}_{H} \to K Fn B$
13	6 11 12	3syl	$⊢ φ \to K Fn B$
14		dffn5	$⊢ K Fn B \leftrightarrow K = (y \in B ⟼ K (y))$
15	13 14	sylib	$⊢ φ \to K = (y \in B ⟼ K (y))$
16		fveq2	$⊢ y = C \to K (y) = K (C)$
17	7 9 15 16	fmptco	$⊢ φ \to K \circ (x \in A ⟼ C) = (x \in A ⟼ K (C))$
18	17	oveq2d	$⊢ φ \to \sum_{H} (K \circ (x \in A ⟼ C)) = \underset{x \in A}{\sum_{H}} K (C)$
19	7	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ B$
20	1 2 3 4 5 6 19 8	gsummhm	$⊢ φ \to \sum_{H} (K \circ (x \in A ⟼ C)) = K (\underset{x \in A}{\sum_{G}} C)$
21	18 20	eqtr3d	$⊢ φ \to \underset{x \in A}{\sum_{H}} K (C) = K (\underset{x \in A}{\sum_{G}} C)$

Metamath Proof Explorer

Theorem gsummptmhm

Proof