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	|- B = ( Base ` G )
	tsmscl.1	|- ( ph -> G e. CMnd )
	tsmscl.2	|- ( ph -> G e. TopSp )
	tsmscl.a	|- ( ph -> A e. V )
	tsmscl.f	|- ( ph -> F : A --> B )
Assertion	tsmscl	|- ( ph -> ( G tsums F ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		tsmscl.b	|- B = ( Base ` G )
2		tsmscl.1	|- ( ph -> G e. CMnd )
3		tsmscl.2	|- ( ph -> G e. TopSp )
4		tsmscl.a	|- ( ph -> A e. V )
5		tsmscl.f	|- ( ph -> F : A --> B )
6		eqid	|- ( TopOpen ` G ) = ( TopOpen ` G )
7		eqid	|- ( ~P A i^i Fin ) = ( ~P A i^i Fin )
8	1 6 7 2 3 4 5	eltsms	|- ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. w e. ( TopOpen ` G ) ( x e. w -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. w ) ) ) ) )
9		simpl	|- ( ( x e. B /\ A. w e. ( TopOpen ` G ) ( x e. w -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. w ) ) ) -> x e. B )
10	8 9	syl6bi	|- ( ph -> ( x e. ( G tsums F ) -> x e. B ) )
11	10	ssrdv	|- ( ph -> ( G tsums F ) C_ B )