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 = inv g ⁡ G
tsmsinv.1 ⊢ φ → G ∈ CMnd
tsmsinv.2 ⊢ φ → G ∈ TopGrp
tsmsinv.a ⊢ φ → A ∈ V
tsmsinv.f ⊢ φ → F : A ⟶ B
tsmsinv.x ⊢ φ → X ∈ G tsums F
Assertion tsmsinv ⊢ φ → I ⁡ X ∈ G tsums I ∘ F

Proof

Step Hyp Ref Expression
1 tsmsinv.b ⊢ B = Base G
2 tsmsinv.p ⊢ I = inv g ⁡ G
3 tsmsinv.1 ⊢ φ → G ∈ CMnd
4 tsmsinv.2 ⊢ φ → G ∈ TopGrp
5 tsmsinv.a ⊢ φ → A ∈ V
6 tsmsinv.f ⊢ φ → F : A ⟶ B
7 tsmsinv.x ⊢ φ → X ∈ G tsums F
8 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
9 tgptps ⊢ G ∈ TopGrp → G ∈ TopSp
10 4 9 syl ⊢ φ → G ∈ TopSp
11 tgpgrp ⊢ G ∈ TopGrp → G ∈ Grp
12 4 11 syl ⊢ φ → G ∈ Grp
13 isabl ⊢ G ∈ Abel ↔ G ∈ Grp ∧ G ∈ CMnd
14 12 3 13 sylanbrc ⊢ φ → G ∈ Abel
15 1 2 invghm ⊢ G ∈ Abel ↔ I ∈ G GrpHom G
16 14 15 sylib ⊢ φ → I ∈ G GrpHom G
17 ghmmhm ⊢ I ∈ G GrpHom G → I ∈ G MndHom G
18 16 17 syl ⊢ φ → I ∈ G MndHom G
19 8 2 tgpinv ⊢ G ∈ TopGrp → I ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
20 4 19 syl ⊢ φ → I ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
21 1 8 8 3 10 3 10 18 20 5 6 7 tsmsmhm ⊢ φ → I ⁡ X ∈ G tsums I ∘ F