Metamath Proof Explorer


Theorem tsmsval

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsval.b
|- B = ( Base ` G )
tsmsval.j
|- J = ( TopOpen ` G )
tsmsval.s
|- S = ( ~P A i^i Fin )
tsmsval.l
|- L = ran ( z e. S |-> { y e. S | z C_ y } )
tsmsval.g
|- ( ph -> G e. V )
tsmsval.a
|- ( ph -> A e. W )
tsmsval.f
|- ( ph -> F : A --> B )
Assertion tsmsval
|- ( ph -> ( G tsums F ) = ( ( J fLimf ( S filGen L ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tsmsval.b
 |-  B = ( Base ` G )
2 tsmsval.j
 |-  J = ( TopOpen ` G )
3 tsmsval.s
 |-  S = ( ~P A i^i Fin )
4 tsmsval.l
 |-  L = ran ( z e. S |-> { y e. S | z C_ y } )
5 tsmsval.g
 |-  ( ph -> G e. V )
6 tsmsval.a
 |-  ( ph -> A e. W )
7 tsmsval.f
 |-  ( ph -> F : A --> B )
8 1 fvexi
 |-  B e. _V
9 8 a1i
 |-  ( ph -> B e. _V )
10 fex2
 |-  ( ( F : A --> B /\ A e. W /\ B e. _V ) -> F e. _V )
11 7 6 9 10 syl3anc
 |-  ( ph -> F e. _V )
12 7 fdmd
 |-  ( ph -> dom F = A )
13 1 2 3 4 5 11 12 tsmsval2
 |-  ( ph -> ( G tsums F ) = ( ( J fLimf ( S filGen L ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) )