Theorem gsumsubm

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

	Ref	Expression
Hypotheses	gsumsubm.a	$$⊢\phi \to A\in V$$
	gsumsubm.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
	gsumsubm.f	$$⊢\phi \to F:A⟶S$$
	gsumsubm.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
Assertion	gsumsubm	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$

Proof

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