Metamath Proof Explorer

Theorem eltsms

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

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 eqid 
 |-  ran ( z e. S |-> { y e. S | z C_ y } ) = ran ( z e. S |-> { y e. S | z C_ y } )
9 1 2 3 8 4 6 7 tsmsval 
 |-  ( ph -> ( G tsums F ) = ( ( J fLimf ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) )
10 9 eleq2d 
 |-  ( ph -> ( C e. ( G tsums F ) <-> C e. ( ( J fLimf ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) ) )
11 1 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
12 5 11 sylib 
 |-  ( ph -> J e. ( TopOn ` B ) )
13 eqid 
 |-  ( z e. S |-> { y e. S | z C_ y } ) = ( z e. S |-> { y e. S | z C_ y } )
14 3 13 8 6 tsmsfbas 
 |-  ( ph -> ran ( z e. S |-> { y e. S | z C_ y } ) e. ( fBas ` S ) )
15 1 3 4 6 7 tsmslem1 
 |-  ( ( ph /\ y e. S ) -> ( G gsum ( F |` y ) ) e. B )
16 15 fmpttd 
 |-  ( ph -> ( y e. S |-> ( G gsum ( F |` y ) ) ) : S --> B )
17 eqid 
 |-  ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) ) = ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) )
18 17 flffbas 
 |-  ( ( J e. ( TopOn ` B ) /\ ran ( z e. S |-> { y e. S | z C_ y } ) e. ( fBas ` S ) /\ ( y e. S |-> ( G gsum ( F |` y ) ) ) : S --> B ) -> ( C e. ( ( J fLimf ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u ) ) ) )
19 12 14 16 18 syl3anc 
 |-  ( ph -> ( C e. ( ( J fLimf ( S filGen ran ( z e. S |-> { y e. S | z C_ y } ) ) ) ` ( y e. S |-> ( G gsum ( F |` y ) ) ) ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u ) ) ) )
20 pwexg 
 |-  ( A e. V -> ~P A e. _V )
21 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
22 6 20 21 3syl 
 |-  ( ph -> ( ~P A i^i Fin ) e. _V )
23 3 22 eqeltrid 
 |-  ( ph -> S e. _V )
24 23 adantr 
 |-  ( ( ph /\ u e. J ) -> S e. _V )
25 rabexg 
 |-  ( S e. _V -> { y e. S | z C_ y } e. _V )
26 24 25 syl 
 |-  ( ( ph /\ u e. J ) -> { y e. S | z C_ y } e. _V )
27 26 ralrimivw 
 |-  ( ( ph /\ u e. J ) -> A. z e. S { y e. S | z C_ y } e. _V )
28 imaeq2 
 |-  ( w = { y e. S | z C_ y } -> ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) = ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) )
29 28 sseq1d 
 |-  ( w = { y e. S | z C_ y } -> ( ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u <-> ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u ) )
30 13 29 rexrnmptw 
 |-  ( A. z e. S { y e. S | z C_ y } e. _V -> ( E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u <-> E. z e. S ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u ) )
31 27 30 syl 
 |-  ( ( ph /\ u e. J ) -> ( E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u <-> E. z e. S ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u ) )
32 funmpt 
 |-  Fun ( y e. S |-> ( G gsum ( F |` y ) ) )
33 ssrab2 
 |-  { y e. S | z C_ y } C_ S
34 ovex 
 |-  ( G gsum ( F |` y ) ) e. _V
35 eqid 
 |-  ( y e. S |-> ( G gsum ( F |` y ) ) ) = ( y e. S |-> ( G gsum ( F |` y ) ) )
36 34 35 dmmpti 
 |-  dom ( y e. S |-> ( G gsum ( F |` y ) ) ) = S
37 33 36 sseqtrri 
 |-  { y e. S | z C_ y } C_ dom ( y e. S |-> ( G gsum ( F |` y ) ) )
38 funimass3 
 |-  ( ( Fun ( y e. S |-> ( G gsum ( F |` y ) ) ) /\ { y e. S | z C_ y } C_ dom ( y e. S |-> ( G gsum ( F |` y ) ) ) ) -> ( ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u <-> { y e. S | z C_ y } C_ ( `' ( y e. S |-> ( G gsum ( F |` y ) ) ) " u ) ) )
39 32 37 38 mp2an 
 |-  ( ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u <-> { y e. S | z C_ y } C_ ( `' ( y e. S |-> ( G gsum ( F |` y ) ) ) " u ) )
40 35 mptpreima 
 |-  ( `' ( y e. S |-> ( G gsum ( F |` y ) ) ) " u ) = { y e. S | ( G gsum ( F |` y ) ) e. u }
41 40 sseq2i 
 |-  ( { y e. S | z C_ y } C_ ( `' ( y e. S |-> ( G gsum ( F |` y ) ) ) " u ) <-> { y e. S | z C_ y } C_ { y e. S | ( G gsum ( F |` y ) ) e. u } )
42 ss2rab 
 |-  ( { y e. S | z C_ y } C_ { y e. S | ( G gsum ( F |` y ) ) e. u } <-> A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) )
43 39 41 42 3bitri 
 |-  ( ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u <-> A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) )
44 43 rexbii 
 |-  ( E. z e. S ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " { y e. S | z C_ y } ) C_ u <-> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) )
45 31 44 bitrdi 
 |-  ( ( ph /\ u e. J ) -> ( E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u <-> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
46 45 imbi2d 
 |-  ( ( ph /\ u e. J ) -> ( ( C e. u -> E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u ) <-> ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
47 46 ralbidva 
 |-  ( ph -> ( A. u e. J ( C e. u -> E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u ) <-> A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
48 47 anbi2d 
 |-  ( ph -> ( ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S |-> { y e. S | z C_ y } ) ( ( y e. S |-> ( G gsum ( F |` y ) ) ) " w ) C_ u ) ) <-> ( 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 ) ) ) ) )
49 10 19 48 3bitrd 
 |-  ( 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 ) ) ) ) )