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