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	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) → 𝑥 ∈ 𝐵 ) )
11	10	ssrdv	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )