Metamath Proof Explorer

Theorem tsmsxp

Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b 
|- B = ( Base ` G )
tsmsxp.g 
|- ( ph -> G e. CMnd )
tsmsxp.2 
|- ( ph -> G e. TopGrp )
tsmsxp.a 
|- ( ph -> A e. V )
tsmsxp.c 
|- ( ph -> C e. W )
tsmsxp.f 
|- ( ph -> F : ( A X. C ) --> B )
tsmsxp.h 
|- ( ph -> H : A --> B )
tsmsxp.1 
|- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
Assertion tsmsxp 
|- ( ph -> ( G tsums F ) C_ ( G tsums H ) )

Proof

Step Hyp Ref Expression
1 tsmsxp.b 
 |-  B = ( Base ` G )
2 tsmsxp.g 
 |-  ( ph -> G e. CMnd )
3 tsmsxp.2 
 |-  ( ph -> G e. TopGrp )
4 tsmsxp.a 
 |-  ( ph -> A e. V )
5 tsmsxp.c 
 |-  ( ph -> C e. W )
6 tsmsxp.f 
 |-  ( ph -> F : ( A X. C ) --> B )
7 tsmsxp.h 
 |-  ( ph -> H : A --> B )
8 tsmsxp.1 
 |-  ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
9 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
10 3 9 syl 
 |-  ( ph -> G e. TopMnd )
11 10 3ad2ant1 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> G e. TopMnd )
12 simp2 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> u e. ( TopOpen ` G ) )
13 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
14 13 1 tmdtopon 
 |-  ( G e. TopMnd -> ( TopOpen ` G ) e. ( TopOn ` B ) )
15 11 14 syl 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( TopOpen ` G ) e. ( TopOn ` B ) )
16 toponss 
 |-  ( ( ( TopOpen ` G ) e. ( TopOn ` B ) /\ u e. ( TopOpen ` G ) ) -> u C_ B )
17 15 12 16 syl2anc 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> u C_ B )
18 simp3 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> x e. u )
19 17 18 sseldd 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> x e. B )
20 tmdmnd 
 |-  ( G e. TopMnd -> G e. Mnd )
21 11 20 syl 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> G e. Mnd )
22 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
23 1 22 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
24 21 23 syl 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( 0g ` G ) e. B )
25 eqid 
 |-  ( +g ` G ) = ( +g ` G )
26 1 25 22 mndrid 
 |-  ( ( G e. Mnd /\ x e. B ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
27 21 19 26 syl2anc 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
28 27 18 eqeltrd 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( x ( +g ` G ) ( 0g ` G ) ) e. u )
29 1 13 25 tmdcn2 
 |-  ( ( ( G e. TopMnd /\ u e. ( TopOpen ` G ) ) /\ ( x e. B /\ ( 0g ` G ) e. B /\ ( x ( +g ` G ) ( 0g ` G ) ) e. u ) ) -> E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) )
30 11 12 19 24 28 29 syl23anc 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) )
31 r19.29 
 |-  ( ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. v e. ( TopOpen ` G ) ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) )
32 simp31 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> x e. v )
33 elfpw 
 |-  ( y e. ( ~P ( A X. C ) i^i Fin ) <-> ( y C_ ( A X. C ) /\ y e. Fin ) )
34 33 simplbi 
 |-  ( y e. ( ~P ( A X. C ) i^i Fin ) -> y C_ ( A X. C ) )
35 34 ad2antrl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> y C_ ( A X. C ) )
36 dmss 
 |-  ( y C_ ( A X. C ) -> dom y C_ dom ( A X. C ) )
37 35 36 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> dom y C_ dom ( A X. C ) )
38 dmxpss 
 |-  dom ( A X. C ) C_ A
39 37 38 sstrdi 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> dom y C_ A )
40 elinel2 
 |-  ( y e. ( ~P ( A X. C ) i^i Fin ) -> y e. Fin )
41 40 ad2antrl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> y e. Fin )
42 dmfi 
 |-  ( y e. Fin -> dom y e. Fin )
43 41 42 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> dom y e. Fin )
44 elfpw 
 |-  ( dom y e. ( ~P A i^i Fin ) <-> ( dom y C_ A /\ dom y e. Fin ) )
45 39 43 44 sylanbrc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> dom y e. ( ~P A i^i Fin ) )
46 eqid 
 |-  ( .g ` G ) = ( .g ` G )
47 simpl11 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ph )
48 47 2 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. CMnd )
49 47 10 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. TopMnd )
50 simprrl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> b e. ( ~P A i^i Fin ) )
51 50 elin2d 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> b e. Fin )
52 simpl2r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> t e. ( TopOpen ` G ) )
53 49 20 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. Mnd )
54 53 23 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( 0g ` G ) e. B )
55 hashcl 
 |-  ( b e. Fin -> ( # ` b ) e. NN0 )
56 51 55 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( # ` b ) e. NN0 )
57 1 46 22 mulgnn0z 
 |-  ( ( G e. Mnd /\ ( # ` b ) e. NN0 ) -> ( ( # ` b ) ( .g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
58 53 56 57 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( ( # ` b ) ( .g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
59 simpl32 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( 0g ` G ) e. t )
60 58 59 eqeltrd 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( ( # ` b ) ( .g ` G ) ( 0g ` G ) ) e. t )
61 13 1 46 48 49 51 52 54 60 tmdgsum2 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> E. s e. ( TopOpen ` G ) ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) )
62 simp111 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> ph )
63 62 2 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> G e. CMnd )
64 62 3 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> G e. TopGrp )
65 62 4 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> A e. V )
66 62 5 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> C e. W )
67 62 6 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> F : ( A X. C ) --> B )
68 62 7 syl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> H : A --> B )
69 62 8 sylan 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
70 eqid 
 |-  ( -g ` G ) = ( -g ` G )
71 simp3l 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> s e. ( TopOpen ` G ) )
72 simp3rl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> ( 0g ` G ) e. s )
73 simp2rl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> b e. ( ~P A i^i Fin ) )
74 simp2rr 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> dom y C_ b )
75 simp2ll 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> y e. ( ~P ( A X. C ) i^i Fin ) )
76 1 63 64 65 66 67 68 69 13 22 25 70 71 72 73 74 75 tsmsxplem1 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> E. n e. ( ~P C i^i Fin ) ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) )
77 48 3adant3 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> G e. CMnd )
78 64 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> G e. TopGrp )
79 65 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A e. V )
80 66 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> C e. W )
81 67 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> F : ( A X. C ) --> B )
82 68 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> H : A --> B )
83 47 3adant3 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ph )
84 83 8 sylan 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
85 simp3ll 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> s e. ( TopOpen ` G ) )
86 72 3adant3r 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( 0g ` G ) e. s )
87 simp2rl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> b e. ( ~P A i^i Fin ) )
88 simp133 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u )
89 simp3rl 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> n e. ( ~P C i^i Fin ) )
90 simp2ll 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> y e. ( ~P ( A X. C ) i^i Fin ) )
91 simp2rr 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> dom y C_ b )
92 simp3rr 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) )
93 92 simpld 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ran y C_ n )
94 relxp 
 |-  Rel ( A X. C )
95 relss 
 |-  ( y C_ ( A X. C ) -> ( Rel ( A X. C ) -> Rel y ) )
96 34 94 95 mpisyl 
 |-  ( y e. ( ~P ( A X. C ) i^i Fin ) -> Rel y )
97 relssdmrn 
 |-  ( Rel y -> y C_ ( dom y X. ran y ) )
98 96 97 syl 
 |-  ( y e. ( ~P ( A X. C ) i^i Fin ) -> y C_ ( dom y X. ran y ) )
99 xpss12 
 |-  ( ( dom y C_ b /\ ran y C_ n ) -> ( dom y X. ran y ) C_ ( b X. n ) )
100 98 99 sylan9ss 
 |-  ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ ( dom y C_ b /\ ran y C_ n ) ) -> y C_ ( b X. n ) )
101 90 91 93 100 syl12anc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> y C_ ( b X. n ) )
102 92 simprd 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s )
103 sseq2 
 |-  ( z = ( b X. n ) -> ( y C_ z <-> y C_ ( b X. n ) ) )
104 reseq2 
 |-  ( z = ( b X. n ) -> ( F |` z ) = ( F |` ( b X. n ) ) )
105 104 oveq2d 
 |-  ( z = ( b X. n ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( b X. n ) ) ) )
106 105 eleq1d 
 |-  ( z = ( b X. n ) -> ( ( G gsum ( F |` z ) ) e. v <-> ( G gsum ( F |` ( b X. n ) ) ) e. v ) )
107 103 106 imbi12d 
 |-  ( z = ( b X. n ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) <-> ( y C_ ( b X. n ) -> ( G gsum ( F |` ( b X. n ) ) ) e. v ) ) )
108 simp2lr 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) )
109 elfpw 
 |-  ( b e. ( ~P A i^i Fin ) <-> ( b C_ A /\ b e. Fin ) )
110 elfpw 
 |-  ( n e. ( ~P C i^i Fin ) <-> ( n C_ C /\ n e. Fin ) )
111 xpss12 
 |-  ( ( b C_ A /\ n C_ C ) -> ( b X. n ) C_ ( A X. C ) )
112 xpfi 
 |-  ( ( b e. Fin /\ n e. Fin ) -> ( b X. n ) e. Fin )
113 111 112 anim12i 
 |-  ( ( ( b C_ A /\ n C_ C ) /\ ( b e. Fin /\ n e. Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
114 113 an4s 
 |-  ( ( ( b C_ A /\ b e. Fin ) /\ ( n C_ C /\ n e. Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
115 109 110 114 syl2anb 
 |-  ( ( b e. ( ~P A i^i Fin ) /\ n e. ( ~P C i^i Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
116 elfpw 
 |-  ( ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) <-> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
117 115 116 sylibr 
 |-  ( ( b e. ( ~P A i^i Fin ) /\ n e. ( ~P C i^i Fin ) ) -> ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) )
118 87 89 117 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) )
119 107 108 118 rspcdva 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( y C_ ( b X. n ) -> ( G gsum ( F |` ( b X. n ) ) ) e. v ) )
120 101 119 mpd 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( G gsum ( F |` ( b X. n ) ) ) e. v )
121 simp3lr 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) )
122 121 simprd 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. g e. ( s ^m b ) ( G gsum g ) e. t )
123 oveq2 
 |-  ( g = h -> ( G gsum g ) = ( G gsum h ) )
124 123 eleq1d 
 |-  ( g = h -> ( ( G gsum g ) e. t <-> ( G gsum h ) e. t ) )
125 124 cbvralvw 
 |-  ( A. g e. ( s ^m b ) ( G gsum g ) e. t <-> A. h e. ( s ^m b ) ( G gsum h ) e. t )
126 122 125 sylib 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. h e. ( s ^m b ) ( G gsum h ) e. t )
127 1 77 78 79 80 81 82 84 13 22 25 70 85 86 87 88 89 101 102 120 126 tsmsxplem2 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( G gsum ( H |` b ) ) e. u )
128 127 3exp 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) -> ( G gsum ( H |` b ) ) e. u ) ) )
129 128 exp4a 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) -> ( ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) -> ( G gsum ( H |` b ) ) e. u ) ) ) )
130 129 3imp1 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsum ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) -> ( G gsum ( H |` b ) ) e. u )
131 76 130 rexlimddv 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> ( G gsum ( H |` b ) ) e. u )
132 131 3expa 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsum g ) e. t ) ) ) -> ( G gsum ( H |` b ) ) e. u )
133 61 132 rexlimddv 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( G gsum ( H |` b ) ) e. u )
134 133 anassrs 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( G gsum ( H |` b ) ) e. u )
135 134 expr 
 |-  ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) /\ b e. ( ~P A i^i Fin ) ) -> ( dom y C_ b -> ( G gsum ( H |` b ) ) e. u ) )
136 135 ralrimiva 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> A. b e. ( ~P A i^i Fin ) ( dom y C_ b -> ( G gsum ( H |` b ) ) e. u ) )
137 sseq1 
 |-  ( a = dom y -> ( a C_ b <-> dom y C_ b ) )
138 137 rspceaimv 
 |-  ( ( dom y e. ( ~P A i^i Fin ) /\ A. b e. ( ~P A i^i Fin ) ( dom y C_ b -> ( G gsum ( H |` b ) ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) )
139 45 136 138 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) )
140 139 rexlimdvaa 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
141 32 140 embantd 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
142 141 3expia 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) ) -> ( ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
143 142 anassrs 
 |-  ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) /\ t e. ( TopOpen ` G ) ) -> ( ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
144 143 rexlimdva 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) -> ( E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
145 144 impcomd 
 |-  ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) -> ( ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
146 145 rexlimdva 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( E. v e. ( TopOpen ` G ) ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
147 31 146 syl5 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) /\ E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
148 30 147 mpan2d 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) )
149 148 3expia 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) ) -> ( x e. u -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
150 149 com23 
 |-  ( ( ph /\ u e. ( TopOpen ` G ) ) -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
151 150 ralrimdva 
 |-  ( ph -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) -> A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) )
152 151 anim2d 
 |-  ( ph -> ( ( x e. B /\ A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) -> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) ) )
153 eqid 
 |-  ( ~P ( A X. C ) i^i Fin ) = ( ~P ( A X. C ) i^i Fin )
154 tgptps 
 |-  ( G e. TopGrp -> G e. TopSp )
155 3 154 syl 
 |-  ( ph -> G e. TopSp )
156 4 5 xpexd 
 |-  ( ph -> ( A X. C ) e. _V )
157 1 13 153 2 155 156 6 eltsms 
 |-  ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. v ) ) ) ) )
158 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
159 1 13 158 2 155 4 7 eltsms 
 |-  ( ph -> ( x e. ( G tsums H ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsum ( H |` b ) ) e. u ) ) ) ) )
160 152 157 159 3imtr4d 
 |-  ( ph -> ( x e. ( G tsums F ) -> x e. ( G tsums H ) ) )
161 160 ssrdv 
 |-  ( ph -> ( G tsums F ) C_ ( G tsums H ) )