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 ⊢ 𝐵 = ( 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 ( 𝐼 ∘ 𝐹 ) ) )