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