Theorem tsmsi

Description: The property of being a sum of the sequence F in the topological commutative monoid G . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	eltsms.b	|- B = ( Base ` G )
	eltsms.j	|- J = ( TopOpen ` G )
	eltsms.s	|- S = ( ~P A i^i Fin )
	eltsms.1	|- ( ph -> G e. CMnd )
	eltsms.2	|- ( ph -> G e. TopSp )
	eltsms.a	|- ( ph -> A e. V )
	eltsms.f	|- ( ph -> F : A --> B )
	tsmsi.3	|- ( ph -> C e. ( G tsums F ) )
	tsmsi.4	|- ( ph -> U e. J )
	tsmsi.5	|- ( ph -> C e. U )
Assertion	tsmsi	|- ( ph -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) )

Proof

Step	Hyp	Ref	Expression
1		eltsms.b	|- B = ( Base ` G )
2		eltsms.j	|- J = ( TopOpen ` G )
3		eltsms.s	|- S = ( ~P A i^i Fin )
4		eltsms.1	|- ( ph -> G e. CMnd )
5		eltsms.2	|- ( ph -> G e. TopSp )
6		eltsms.a	|- ( ph -> A e. V )
7		eltsms.f	|- ( ph -> F : A --> B )
8		tsmsi.3	|- ( ph -> C e. ( G tsums F ) )
9		tsmsi.4	|- ( ph -> U e. J )
10		tsmsi.5	|- ( ph -> C e. U )
11		eleq2	|- ( u = U -> ( C e. u <-> C e. U ) )
12		eleq2	|- ( u = U -> ( ( G gsum ( F |` y ) ) e. u <-> ( G gsum ( F |` y ) ) e. U ) )
13	12	imbi2d	|- ( u = U -> ( ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) <-> ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) ) )
14	13	rexralbidv	|- ( u = U -> ( E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) <-> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) ) )
15	11 14	imbi12d	|- ( u = U -> ( ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) <-> ( C e. U -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) ) ) )
16	1 2 3 4 5 6 7	eltsms	|- ( ph -> ( C e. ( G tsums F ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) ) )
17	8 16	mpbid	|- ( ph -> ( C e. B /\ A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
18	17	simprd	|- ( ph -> A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
19	15 18 9	rspcdva	|- ( ph -> ( C e. U -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) ) )
20	10 19	mpd	|- ( ph -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. U ) )