gsumsubm

Description: Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014)

Step	Hyp	Ref	Expression
1		gsumsubm.a	$⊢ φ \to A \in V$
2		gsumsubm.s	$⊢ φ \to S \in SubMnd (G)$
3		gsumsubm.f	$⊢ φ \to F : A ⟶ S$
4		gsumsubm.h	$⊢ H = G ↾_{𝑠} S$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6		eqid	$⊢ +_{G} = +_{G}$
7		submrcl	$⊢ S \in SubMnd (G) \to G \in Mnd$
8	2 7	syl	$⊢ φ \to G \in Mnd$
9	5	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
10	2 9	syl	$⊢ φ \to S \subseteq {Base}_{G}$
11		eqid	$⊢ 0_{G} = 0_{G}$
12	11	subm0cl	$⊢ S \in SubMnd (G) \to 0_{G} \in S$
13	2 12	syl	$⊢ φ \to 0_{G} \in S$
14	5 6 11	mndlrid	$⊢ (G \in Mnd \land x \in {Base}_{G}) \to (0_{G} +_{G} x = x \land x +_{G} 0_{G} = x)$
15	8 14	sylan	$⊢ (φ \land x \in {Base}_{G}) \to (0_{G} +_{G} x = x \land x +_{G} 0_{G} = x)$
16	5 6 4 8 1 10 3 13 15	gsumress	$⊢ φ \to \sum_{G} F = \sum_{H} F$

Metamath Proof Explorer