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 ) ) ) ) ) |
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 ) ) ) ) ) |