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 
|- 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 biimtrdi 
 |-  ( ph -> ( x e. ( G tsums F ) -> x e. B ) )
11 10 ssrdv 
 |-  ( ph -> ( G tsums F ) C_ B )