Theorem gsumsubm

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

	Ref	Expression
Hypotheses	gsumsubm.a	|- ( ph -> A e. V )
	gsumsubm.s	|- ( ph -> S e. ( SubMnd ` G ) )
	gsumsubm.f	|- ( ph -> F : A --> S )
	gsumsubm.h	|- H = ( G |`s S )
Assertion	gsumsubm	|- ( ph -> ( G gsum F ) = ( H gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsubm.a	|- ( ph -> A e. V )
2		gsumsubm.s	|- ( ph -> S e. ( SubMnd ` G ) )
3		gsumsubm.f	|- ( ph -> F : A --> S )
4		gsumsubm.h	|- H = ( G |`s S )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7		submrcl	|- ( S e. ( SubMnd ` G ) -> G e. Mnd )
8	2 7	syl	|- ( ph -> G e. Mnd )
9	5	submss	|- ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
10	2 9	syl	|- ( ph -> S C_ ( Base ` G ) )
11		eqid	|- ( 0g ` G ) = ( 0g ` G )
12	11	subm0cl	|- ( S e. ( SubMnd ` G ) -> ( 0g ` G ) e. S )
13	2 12	syl	|- ( ph -> ( 0g ` G ) e. S )
14	5 6 11	mndlrid	|- ( ( G e. Mnd /\ x e. ( Base ` G ) ) -> ( ( ( 0g ` G ) ( +g ` G ) x ) = x /\ ( x ( +g ` G ) ( 0g ` G ) ) = x ) )
15	8 14	sylan	|- ( ( ph /\ x e. ( Base ` G ) ) -> ( ( ( 0g ` G ) ( +g ` G ) x ) = x /\ ( x ( +g ` G ) ( 0g ` G ) ) = x ) )
16	5 6 4 8 1 10 3 13 15	gsumress	|- ( ph -> ( G gsum F ) = ( H gsum F ) )