This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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