MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tsmsxp Unicode version

Theorem tsmsxp 17837
Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 15227 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 17835 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015.)
Hypotheses
Ref Expression
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
Ref Expression
tsmsxp  |-  ( ph  ->  ( G tsums  F ) 
C_  ( G tsums  H
) )
Distinct variable groups:    j, k, G    B, k    A, j, k    j, H, k    C, j, k    j, F, k    ph, j, k
Allowed substitution hints:    B( j)    V( j, k)    W( j, k)

Proof of Theorem tsmsxp
Dummy variables  g 
y  z  a  b  c  d  h  n  s  t  u  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsxp.2 . . . . . . . . . . 11  |-  ( ph  ->  G  e.  TopGrp )
2 tgptmd 17762 . . . . . . . . . . 11  |-  ( G  e.  TopGrp  ->  G  e. TopMnd )
31, 2syl 15 . . . . . . . . . 10  |-  ( ph  ->  G  e. TopMnd )
433ad2ant1 976 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  G  e. TopMnd )
5 simp2 956 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  u  e.  ( TopOpen `  G )
)
6 eqid 2283 . . . . . . . . . . . . 13  |-  ( TopOpen `  G )  =  (
TopOpen `  G )
7 tsmsxp.b . . . . . . . . . . . . 13  |-  B  =  ( Base `  G
)
86, 7tmdtopon 17764 . . . . . . . . . . . 12  |-  ( G  e. TopMnd  ->  ( TopOpen `  G
)  e.  (TopOn `  B ) )
94, 8syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  ( TopOpen `  G )  e.  (TopOn `  B ) )
10 toponss 16667 . . . . . . . . . . 11  |-  ( ( ( TopOpen `  G )  e.  (TopOn `  B )  /\  u  e.  ( TopOpen
`  G ) )  ->  u  C_  B
)
119, 5, 10syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  u  C_  B
)
12 simp3 957 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  x  e.  u )
1311, 12sseldd 3181 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  x  e.  B )
14 tmdmnd 17758 . . . . . . . . . . 11  |-  ( G  e. TopMnd  ->  G  e.  Mnd )
154, 14syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  G  e.  Mnd )
16 eqid 2283 . . . . . . . . . . 11  |-  ( 0g
`  G )  =  ( 0g `  G
)
177, 16mndidcl 14391 . . . . . . . . . 10  |-  ( G  e.  Mnd  ->  ( 0g `  G )  e.  B )
1815, 17syl 15 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  ( 0g `  G )  e.  B
)
19 eqid 2283 . . . . . . . . . . . 12  |-  ( +g  `  G )  =  ( +g  `  G )
207, 19, 16mndrid 14394 . . . . . . . . . . 11  |-  ( ( G  e.  Mnd  /\  x  e.  B )  ->  ( x ( +g  `  G ) ( 0g
`  G ) )  =  x )
2115, 13, 20syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  ( x
( +g  `  G ) ( 0g `  G
) )  =  x )
2221, 12eqeltrd 2357 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( TopOpen `  G )  /\  x  e.  u
)  ->  ( x
( +g  `  G ) ( 0g `  G
) )  e.  u
)
237, 6, 19tmdcn2 17772 . . . . . . . . 9  |-  ( ( ( 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
) )
244, 5, 13, 18, 22, 23syl23anc 1189 . . . . . . . 8  |-  ( (
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 ) )
25 r19.29 2683 . . . . . . . . 9  |-  ( ( 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  gsumg  ( 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  gsumg  ( 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
) ) )
26 simp31 991 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 )
27 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( ~P ( A  X.  C )  i^i 
Fin )  <->  ( y  C_  ( A  X.  C
)  /\  y  e.  Fin ) )
2827simplbi 446 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  y  C_  ( A  X.  C
) )
2928ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  y  C_  ( A  X.  C ) )
30 dmss 4878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y 
C_  ( A  X.  C )  ->  dom  y  C_  dom  ( A  X.  C ) )
3129, 30syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  dom  y  C_  dom  ( A  X.  C
) )
32 dmxpss 5107 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  ( A  X.  C )  C_  A
3331, 32syl6ss 3191 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  dom  y  C_  A )
3427simprbi 450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  y  e.  Fin )
3534ad2antrl 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  y  e.  Fin )
36 dmfi 7139 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  Fin  ->  dom  y  e.  Fin )
3735, 36syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  dom  y  e.  Fin )
38 elfpw 7157 . . . . . . . . . . . . . . . . . . . 20  |-  ( dom  y  e.  ( ~P A  i^i  Fin )  <->  ( dom  y  C_  A  /\  dom  y  e.  Fin ) )
3933, 37, 38sylanbrc 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  dom  y  e.  ( ~P A  i^i  Fin ) )
40 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (.g `  G
)  =  (.g `  G
)
41 simpl11 1030 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  ->  ph )
42 tsmsxp.g . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  G  e. CMnd )
4341, 42syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  ->  G  e. CMnd )
4441, 3syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  ->  G  e. TopMnd )
45 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
b  e.  ( ~P A  i^i  Fin )
)
46 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( b  e.  ( ~P A  i^i  Fin )  <->  ( b  C_  A  /\  b  e. 
Fin ) )
4746simprbi 450 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( b  e.  ( ~P A  i^i  Fin )  ->  b  e.  Fin )
4845, 47syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
b  e.  Fin )
49 simpl2r 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
t  e.  ( TopOpen `  G ) )
5044, 14syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  ->  G  e.  Mnd )
5150, 17syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( 0g `  G
)  e.  B )
52 hashcl 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  Fin  ->  ( # `
 b )  e. 
NN0 )
5348, 52syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( # `  b )  e.  NN0 )
547, 40, 16mulgnn0z 14587 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( G  e.  Mnd  /\  ( # `  b )  e.  NN0 )  -> 
( ( # `  b
) (.g `  G ) ( 0g `  G ) )  =  ( 0g
`  G ) )
5550, 53, 54syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( ( # `  b
) (.g `  G ) ( 0g `  G ) )  =  ( 0g
`  G ) )
56 simpl32 1037 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( 0g `  G
)  e.  t )
5755, 56eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( ( # `  b
) (.g `  G ) ( 0g `  G ) )  e.  t )
586, 7, 40, 43, 44, 48, 49, 51, 57tmdgsum2 17779 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )
59 simp111 1084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  ph )
6059, 42syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  G  e. CMnd )
6159, 1syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  G  e.  TopGrp )
62 tsmsxp.a . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A  e.  V )
6359, 62syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  A  e.  V )
64 tsmsxp.c . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  C  e.  W )
6559, 64syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  C  e.  W )
66 tsmsxp.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  F : ( A  X.  C ) --> B )
6759, 66syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  F : ( A  X.  C ) --> B )
68 tsmsxp.h . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  H : A --> B )
6959, 68syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  H : A --> B )
70 tsmsxp.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  ( G tsums  ( k  e.  C  |->  ( j F k ) ) ) )
7159, 70sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  /\  j  e.  A )  ->  ( H `  j
)  e.  ( G tsums 
( k  e.  C  |->  ( j F k ) ) ) )
72 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -g `  G )  =  (
-g `  G )
73 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
s  e.  ( TopOpen `  G ) )
74 simp3rl 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
( 0g `  G
)  e.  s )
75 simp2rl 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
b  e.  ( ~P A  i^i  Fin )
)
76 simp2rr 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  dom  y  C_  b )
77 simp2ll 1022 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
y  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
787, 60, 61, 63, 65, 67, 69, 71, 6, 16, 19, 72, 73, 74, 75, 76, 77tsmsxplem1 17835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  E. n  e.  ( ~P C  i^i  Fin )
( ran  y  C_  n  /\  A. x  e.  b  ( ( H `
 x ) (
-g `  G )
( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) )
79433adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  G  e. CMnd )
80613adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  G  e.  TopGrp )
81633adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A  e.  V )
82653adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  C  e.  W )
83673adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  F : ( A  X.  C ) --> B )
84693adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  H : A --> B )
85413adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  ph )
8685, 70sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  /\  j  e.  A )  ->  ( H `  j
)  e.  ( G tsums 
( k  e.  C  |->  ( j F k ) ) ) )
87 simp3ll 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
s  e.  ( TopOpen `  G ) )
88743adant3r 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( 0g `  G
)  e.  s )
89 simp2rl 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
b  e.  ( ~P A  i^i  Fin )
)
90 simp133 1092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A. c  e.  v  A. d  e.  t 
( c ( +g  `  G ) d )  e.  u )
91 simp3rl 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  n  e.  ( ~P C  i^i  Fin ) )
92 simp2ll 1022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
y  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
93 simp2rr 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  dom  y  C_  b )
94 simp3rr 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( ran  y  C_  n  /\  A. x  e.  b  ( ( H `
 x ) (
-g `  G )
( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) )
9594simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  ran  y  C_  n )
96 relxp 4794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  Rel  ( A  X.  C )
97 relss 4775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y 
C_  ( A  X.  C )  ->  ( Rel  ( A  X.  C
)  ->  Rel  y ) )
9828, 96, 97ee10 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  Rel  y )
99 relssdmrn 5193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( Rel  y  ->  y  C_  ( dom  y  X.  ran  y ) )
10098, 99syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  y  C_  ( dom  y  X. 
ran  y ) )
101 xpss12 4792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( dom  y  C_  b  /\  ran  y  C_  n
)  ->  ( dom  y  X.  ran  y ) 
C_  ( b  X.  n ) )
102100, 101sylan9ss 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( y  e.  ( ~P ( A  X.  C
)  i^i  Fin )  /\  ( dom  y  C_  b  /\  ran  y  C_  n ) )  -> 
y  C_  ( b  X.  n ) )
10392, 93, 95, 102syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
y  C_  ( b  X.  n ) )
10494simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A. x  e.  b 
( ( H `  x ) ( -g `  G ) ( G 
gsumg  ( F  |`  ( { x }  X.  n
) ) ) )  e.  s )
105 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  e.  ( ~P C  i^i  Fin )  <->  ( n  C_  C  /\  n  e. 
Fin ) )
106 xpss12 4792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( b  C_  A  /\  n  C_  C )  -> 
( b  X.  n
)  C_  ( A  X.  C ) )
107 xpfi 7128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( b  e.  Fin  /\  n  e.  Fin )  ->  ( b  X.  n
)  e.  Fin )
108106, 107anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( b  C_  A  /\  n  C_  C )  /\  ( b  e. 
Fin  /\  n  e.  Fin ) )  ->  (
( b  X.  n
)  C_  ( A  X.  C )  /\  (
b  X.  n )  e.  Fin ) )
109108an4s 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( b  C_  A  /\  b  e.  Fin )  /\  ( n  C_  C  /\  n  e.  Fin ) )  ->  (
( b  X.  n
)  C_  ( A  X.  C )  /\  (
b  X.  n )  e.  Fin ) )
11046, 105, 109syl2anb 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 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 ) )
111 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( b  X.  n )  e.  ( ~P ( A  X.  C )  i^i 
Fin )  <->  ( (
b  X.  n ) 
C_  ( A  X.  C )  /\  (
b  X.  n )  e.  Fin ) )
112110, 111sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 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 ) )
11389, 91, 112syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( b  X.  n
)  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
114 simp2lr 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A. z  e.  ( ~P ( A  X.  C
)  i^i  Fin )
( y  C_  z  ->  ( G  gsumg  ( F  |`  z
) )  e.  v ) )
115 sseq2 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  ( b  X.  n )  ->  (
y  C_  z  <->  y  C_  ( b  X.  n
) ) )
116 reseq2 4950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z  =  ( b  X.  n )  ->  ( F  |`  z )  =  ( F  |`  (
b  X.  n ) ) )
117116oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( z  =  ( b  X.  n )  ->  ( G  gsumg  ( F  |`  z
) )  =  ( G  gsumg  ( F  |`  (
b  X.  n ) ) ) )
118117eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  =  ( b  X.  n )  ->  (
( G  gsumg  ( F  |`  z
) )  e.  v  <-> 
( G  gsumg  ( F  |`  (
b  X.  n ) ) )  e.  v ) )
119115, 118imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z  =  ( b  X.  n )  ->  (
( y  C_  z  ->  ( G  gsumg  ( F  |`  z
) )  e.  v )  <->  ( y  C_  ( b  X.  n
)  ->  ( G  gsumg  ( F  |`  ( b  X.  n ) ) )  e.  v ) ) )
120119rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( b  X.  n )  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  ( A. z  e.  ( ~P ( A  X.  C
)  i^i  Fin )
( y  C_  z  ->  ( G  gsumg  ( F  |`  z
) )  e.  v )  ->  ( y  C_  ( b  X.  n
)  ->  ( G  gsumg  ( F  |`  ( b  X.  n ) ) )  e.  v ) ) )
121113, 114, 103, 120syl3c 57 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( G  gsumg  ( F  |`  (
b  X.  n ) ) )  e.  v )
122 simp3lr 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( ( 0g `  G )  e.  s  /\  A. g  e.  ( s  ^m  b
) ( G  gsumg  g )  e.  t ) )
123122simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A. g  e.  (
s  ^m  b )
( G  gsumg  g )  e.  t )
124 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( g  =  h  ->  ( G  gsumg  g )  =  ( G  gsumg  h ) )
125124eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( g  =  h  ->  (
( G  gsumg  g )  e.  t  <-> 
( G  gsumg  h )  e.  t ) )
126125cbvralv 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( A. g  e.  ( s  ^m  b ) ( G 
gsumg  g )  e.  t  <->  A. h  e.  (
s  ^m  b )
( G  gsumg  h )  e.  t )
127123, 126sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  ->  A. h  e.  (
s  ^m  b )
( G  gsumg  h )  e.  t )
1287, 79, 80, 81, 82, 83, 84, 86, 6, 16, 19, 72, 87, 88, 89, 90, 91, 103, 104, 121, 127tsmsxplem2 17836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) ) )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
)
1291283exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) )  ->  ( G  gsumg  ( H  |`  b
) )  e.  u
) ) )
130129exp4a 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) )  ->  ( ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) )  ->  ( G  gsumg  ( H  |`  b )
)  e.  u ) ) ) )
1311303imp1 1164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  /\  ( n  e.  ( ~P C  i^i  Fin )  /\  ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `
 x ) (
-g `  G )
( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s ) ) )  ->  ( G  gsumg  ( H  |`  b
) )  e.  u
)
132131expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  /\  n  e.  ( ~P C  i^i  Fin ) )  ->  ( ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x
) ( -g `  G
) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s )  ->  ( G  gsumg  ( H  |`  b ) )  e.  u ) )
133132rexlimdva 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
( E. n  e.  ( ~P C  i^i  Fin ) ( ran  y  C_  n  /\  A. x  e.  b  ( ( H `  x )
( -g `  G ) ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  s )  ->  ( G  gsumg  ( H  |`  b ) )  e.  u ) )
13478, 133mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
)
1351343expa 1151 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t ) ) )  ->  ( G  gsumg  ( H  |`  b )
)  e.  u )
136135expr 598 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
) )
137136rexlimdva 2667 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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  gsumg  ( 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  gsumg  g )  e.  t )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
) )
13858, 137mpd 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v ) )  /\  (
b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b
) ) )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
)
139138anassrs 629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  /\  ( b  e.  ( ~P A  i^i  Fin )  /\  dom  y  C_  b ) )  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
)
140139expr 598 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  /\  b  e.  ( ~P A  i^i  Fin ) )  ->  ( dom  y  C_  b  -> 
( G  gsumg  ( H  |`  b
) )  e.  u
) )
141140ralrimiva 2626 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  A. b  e.  ( ~P A  i^i  Fin ) ( dom  y  C_  b  ->  ( G  gsumg  ( H  |`  b )
)  e.  u ) )
142 sseq1 3199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  dom  y  -> 
( a  C_  b  <->  dom  y  C_  b )
)
143142imbi1d 308 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  dom  y  -> 
( ( a  C_  b  ->  ( G  gsumg  ( H  |`  b ) )  e.  u )  <->  ( dom  y  C_  b  ->  ( G  gsumg  ( H  |`  b
) )  e.  u
) ) )
144143ralbidv 2563 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  dom  y  -> 
( A. b  e.  ( ~P A  i^i  Fin ) ( a  C_  b  ->  ( G  gsumg  ( H  |`  b ) )  e.  u )  <->  A. b  e.  ( ~P A  i^i  Fin ) ( dom  y  C_  b  ->  ( G  gsumg  ( H  |`  b )
)  e.  u ) ) )
145144rspcev 2884 . . . . . . . . . . . . . . . . . . 19  |-  ( ( dom  y  e.  ( ~P A  i^i  Fin )  /\  A. b  e.  ( ~P A  i^i  Fin ) ( dom  y  C_  b  ->  ( G  gsumg  ( H  |`  b )
)  e.  u ) )  ->  E. a  e.  ( ~P A  i^i  Fin ) A. b  e.  ( ~P A  i^i  Fin ) ( a  C_  b  ->  ( G  gsumg  ( H  |`  b ) )  e.  u ) )
14639, 141, 145syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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  gsumg  ( F  |`  z ) )  e.  v ) ) )  ->  E. a  e.  ( ~P A  i^i  Fin ) A. b  e.  ( ~P A  i^i  Fin ) ( a  C_  b  ->  ( G  gsumg  ( H  |`  b ) )  e.  u ) )
147146expr 598 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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  gsumg  ( F  |`  z
) )  e.  v )  ->  E. a  e.  ( ~P A  i^i  Fin ) A. b  e.  ( ~P A  i^i  Fin ) ( a  C_  b  ->  ( G  gsumg  ( H  |`  b ) )  e.  u ) ) )
148147rexlimdva 2667 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 (