tsmsinv

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

Step	Hyp	Ref	Expression
1		tsmsinv.b	$⊢ B = {Base}_{G}$
2		tsmsinv.p	$⊢ I = {inv}_{g} (G)$
3		tsmsinv.1	$⊢ φ \to G \in CMnd$
4		tsmsinv.2	$⊢ φ \to G \in TopGrp$
5		tsmsinv.a	$⊢ φ \to A \in V$
6		tsmsinv.f	$⊢ φ \to F : A ⟶ B$
7		tsmsinv.x	$⊢ φ \to X \in (G tsums F)$
8		eqid	$⊢ TopOpen (G) = TopOpen (G)$
9		tgptps	$⊢ G \in TopGrp \to G \in TopSp$
10	4 9	syl	$⊢ φ \to G \in TopSp$
11		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
12	4 11	syl	$⊢ φ \to G \in Grp$
13		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
14	12 3 13	sylanbrc	$⊢ φ \to G \in Abel$
15	1 2	invghm	$⊢ G \in Abel \leftrightarrow I \in (G GrpHom G)$
16	14 15	sylib	$⊢ φ \to I \in (G GrpHom G)$
17		ghmmhm	$⊢ I \in (G GrpHom G) \to I \in (G MndHom G)$
18	16 17	syl	$⊢ φ \to I \in (G MndHom G)$
19	8 2	tgpinv	$⊢ G \in TopGrp \to I \in (TopOpen (G) Cn TopOpen (G))$
20	4 19	syl	$⊢ φ \to I \in (TopOpen (G) Cn TopOpen (G))$
21	1 8 8 3 10 3 10 18 20 5 6 7	tsmsmhm	$⊢ φ \to I (X) \in (G tsums (I \circ F))$

Metamath Proof Explorer