Metamath Proof Explorer


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 ) )