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

Metamath Proof Explorer

Theorem gsuminv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 4-May-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsuminv.b 
|- B = ( Base ` G )
gsuminv.z 
|- .0. = ( 0g ` G )
gsuminv.p 
|- I = ( invg ` G )
gsuminv.g 
|- ( ph -> G e. Abel )
gsuminv.a 
|- ( ph -> A e. V )
gsuminv.f 
|- ( ph -> F : A --> B )
gsuminv.n 
|- ( ph -> F finSupp .0. )
Assertion gsuminv 
|- ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )

Proof

Step Hyp Ref Expression
1 gsuminv.b 
 |-  B = ( Base ` G )
2 gsuminv.z 
 |-  .0. = ( 0g ` G )
3 gsuminv.p 
 |-  I = ( invg ` G )
4 gsuminv.g 
 |-  ( ph -> G e. Abel )
5 gsuminv.a 
 |-  ( ph -> A e. V )
6 gsuminv.f 
 |-  ( ph -> F : A --> B )
7 gsuminv.n 
 |-  ( ph -> F finSupp .0. )
8 ablcmn 
 |-  ( G e. Abel -> G e. CMnd )
9 4 8 syl 
 |-  ( ph -> G e. CMnd )
10 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
11 9 10 syl 
 |-  ( ph -> G e. Mnd )
12 1 3 invghm 
 |-  ( G e. Abel <-> I e. ( G GrpHom G ) )
13 4 12 sylib 
 |-  ( ph -> I e. ( G GrpHom G ) )
14 ghmmhm 
 |-  ( I e. ( G GrpHom G ) -> I e. ( G MndHom G ) )
15 13 14 syl 
 |-  ( ph -> I e. ( G MndHom G ) )
16 1 2 9 11 5 15 6 7 gsummhm 
 |-  ( ph -> ( G gsum ( I o. F ) ) = ( I ` ( G gsum F ) ) )