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

Metamath Proof Explorer

Theorem tsmsinv

Description: Inverse of an infinite group sum. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses tsmsinv.b 
|- B = ( Base ` G )
tsmsinv.p 
|- I = ( invg ` G )
tsmsinv.1 
|- ( ph -> G e. CMnd )
tsmsinv.2 
|- ( ph -> G e. TopGrp )
tsmsinv.a 
|- ( ph -> A e. V )
tsmsinv.f 
|- ( ph -> F : A --> B )
tsmsinv.x 
|- ( ph -> X e. ( G tsums F ) )
Assertion tsmsinv 
|- ( ph -> ( I ` X ) e. ( G tsums ( I o. F ) ) )

Proof

Step Hyp Ref Expression
1 tsmsinv.b 
 |-  B = ( Base ` G )
2 tsmsinv.p 
 |-  I = ( invg ` G )
3 tsmsinv.1 
 |-  ( ph -> G e. CMnd )
4 tsmsinv.2 
 |-  ( ph -> G e. TopGrp )
5 tsmsinv.a 
 |-  ( ph -> A e. V )
6 tsmsinv.f 
 |-  ( ph -> F : A --> B )
7 tsmsinv.x 
 |-  ( ph -> X e. ( G tsums F ) )
8 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
9 tgptps 
 |-  ( G e. TopGrp -> G e. TopSp )
10 4 9 syl 
 |-  ( ph -> G e. TopSp )
11 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
12 4 11 syl 
 |-  ( ph -> G e. Grp )
13 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
14 12 3 13 sylanbrc 
 |-  ( ph -> G e. Abel )
15 1 2 invghm 
 |-  ( G e. Abel <-> I e. ( G GrpHom G ) )
16 14 15 sylib 
 |-  ( ph -> I e. ( G GrpHom G ) )
17 ghmmhm 
 |-  ( I e. ( G GrpHom G ) -> I e. ( G MndHom G ) )
18 16 17 syl 
 |-  ( ph -> I e. ( G MndHom G ) )
19 8 2 tgpinv 
 |-  ( G e. TopGrp -> I e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
20 4 19 syl 
 |-  ( ph -> I e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
21 1 8 8 3 10 3 10 18 20 5 6 7 tsmsmhm 
 |-  ( ph -> ( I ` X ) e. ( G tsums ( I o. F ) ) )