This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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