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 |`s B )
	gsumsubg.a	|- ( ph -> A e. V )
	gsumsubg.f	|- ( ph -> F : A --> B )
	gsumsubg.b	|- ( ph -> B e. ( SubGrp ` G ) )
Assertion	gsumsubg	|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsubg.1	|- H = ( G |`s B )
2		gsumsubg.a	|- ( ph -> A e. V )
3		gsumsubg.f	|- ( ph -> F : A --> B )
4		gsumsubg.b	|- ( ph -> B e. ( SubGrp ` G ) )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7	4	elfvexd	|- ( ph -> G e. _V )
8	5	subgss	|- ( B e. ( SubGrp ` G ) -> B C_ ( Base ` G ) )
9	4 8	syl	|- ( ph -> B C_ ( Base ` G ) )
10		eqid	|- ( 0g ` G ) = ( 0g ` G )
11	10	subg0cl	|- ( B e. ( SubGrp ` G ) -> ( 0g ` G ) e. B )
12	4 11	syl	|- ( ph -> ( 0g ` G ) e. B )
13		subgrcl	|- ( B e. ( SubGrp ` G ) -> G e. Grp )
14	4 13	syl	|- ( ph -> G e. Grp )
15	5 6 10	grplid	|- ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( 0g ` G ) ( +g ` G ) x ) = x )
16	5 6 10	grprid	|- ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
17	15 16	jca	|- ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( ( 0g ` G ) ( +g ` G ) x ) = x /\ ( x ( +g ` G ) ( 0g ` G ) ) = x ) )
18	14 17	sylan	|- ( ( ph /\ x e. ( Base ` G ) ) -> ( ( ( 0g ` G ) ( +g ` G ) x ) = x /\ ( x ( +g ` G ) ( 0g ` G ) ) = x ) )
19	5 6 1 7 2 9 3 12 18	gsumress	|- ( ph -> ( G gsum F ) = ( H gsum F ) )