Theorem tsmsinv

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

	Ref	Expression
Hypotheses	tsmsinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tsmsinv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
	tsmsinv.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	tsmsinv.2	⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
	tsmsinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	tsmsinv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	tsmsinv.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
Assertion	tsmsinv	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝐺 tsums ( 𝐼 ∘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tsmsinv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tsmsinv.p	⊢ 𝐼 = ( invg ‘ 𝐺 )
3		tsmsinv.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		tsmsinv.2	⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
5		tsmsinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		tsmsinv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		tsmsinv.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
8		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
9		tgptps	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
10	4 9	syl	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
11		tgpgrp	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
12	4 11	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
13		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
14	12 3 13	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ Abel )
15	1 2	invghm	⊢ ( 𝐺 ∈ Abel ↔ 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
16	14 15	sylib	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
17		ghmmhm	⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
18	16 17	syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
19	8 2	tgpinv	⊢ ( 𝐺 ∈ TopGrp → 𝐼 ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
20	4 19	syl	⊢ ( 𝜑 → 𝐼 ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
21	1 8 8 3 10 3 10 18 20 5 6 7	tsmsmhm	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝐺 tsums ( 𝐼 ∘ 𝐹 ) ) )