Theorem gsumsubg

Description: The group sum in a subgroup is the same as the group sum. (Contributed by Thierry Arnoux, 28-May-2023)

	Ref	Expression
Hypotheses	gsumsubg.1	$$⊢H=G{\upharpoonright }_{𝑠}B$$
	gsumsubg.a	$$⊢\phi \to A\in V$$
	gsumsubg.f	$$⊢\phi \to F:A⟶B$$
	gsumsubg.b	$$⊢\phi \to B\in \mathrm{SubGrp}\left(G\right)$$
Assertion	gsumsubg	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$

Proof

Step	Hyp	Ref	Expression
1		gsumsubg.1	$$⊢H=G{\upharpoonright }_{𝑠}B$$
2		gsumsubg.a	$$⊢\phi \to A\in V$$
3		gsumsubg.f	$$⊢\phi \to F:A⟶B$$
4		gsumsubg.b	$$⊢\phi \to B\in \mathrm{SubGrp}\left(G\right)$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6		eqid	$$⊢{+}_G={+}_G$$
7	4	elfvexd	$$⊢\phi \to G\in \mathrm{V}$$
8	5	subgss	$$⊢B\in \mathrm{SubGrp}\left(G\right)\to B\subseteq {\mathrm{Base}}_G$$
9	4 8	syl	$$⊢\phi \to B\subseteq {\mathrm{Base}}_G$$
10		eqid	$$⊢0_G=0_G$$
11	10	subg0cl	$$⊢B\in \mathrm{SubGrp}\left(G\right)\to 0_G\in B$$
12	4 11	syl	$$⊢\phi \to 0_G\in B$$
13		subgrcl	$$⊢B\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
14	4 13	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
15	5 6 10	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\right)\to 0_G{+}_{G}x=x$$
16	5 6 10	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\right)\to x{+}_G{0}_G=x$$
17	15 16	jca	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\right)\to \left(0_G{+}_{G}x=x\wedge x{+}_G{0}_G=x\right)$$
18	14 17	sylan	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \left(0_G{+}_{G}x=x\wedge x{+}_G{0}_G=x\right)$$
19	5 6 1 7 2 9 3 12 18	gsumress	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$