This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tsmscl

Description: A sum in a topological group is an element of the group. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmscl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion tsmscl ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 tsmscl.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmscl.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3 tsmscl.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4 tsmscl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 tsmscl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
7 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
8 1 6 7 2 3 4 5 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑤 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑤 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑤 ) ) ) ) )
9 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑤 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑤 → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑤 ) ) ) → 𝑥 ∈ 𝐵 )
10 8 9 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 ∈ 𝐵 ) )
11 10 ssrdv ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )