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

Theorem tsmsxplem1 19569
Description: Lemma for tsmsxp 19571. (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 ) ) ) )
tsmsxp.j  |-  J  =  ( TopOpen `  G )
tsmsxp.z  |-  .0.  =  ( 0g `  G )
tsmsxp.p  |-  .+  =  ( +g  `  G )
tsmsxp.m  |-  .-  =  ( -g `  G )
tsmsxp.l  |-  ( ph  ->  L  e.  J )
tsmsxp.3  |-  ( ph  ->  .0.  e.  L )
tsmsxp.k  |-  ( ph  ->  K  e.  ( ~P A  i^i  Fin )
)
tsmsxp.ks  |-  ( ph  ->  dom  D  C_  K
)
tsmsxp.d  |-  ( ph  ->  D  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
Assertion
Ref Expression
tsmsxplem1  |-  ( ph  ->  E. n  e.  ( ~P C  i^i  Fin ) ( ran  D  C_  n  /\  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L ) )
Distinct variable groups:    .0. , k    j, k, n, x, G    B, k    D, j, k, n, x    j, L, n, x    A, j, k, n    j, K, k, n, x    j, H, k, n, x    .- , j, n, x    C, j, k, n    j, F, k, n, x    ph, j,
k, n
Allowed substitution hints:    ph( x)    A( x)    B( x, j, n)    C( x)    .+ ( x, j, k, n)    J( x, j, k, n)    L( k)    .- ( k)    V( x, j, k, n)    W( x, j, k, n)    .0. ( x, j, n)

Proof of Theorem tsmsxplem1
Dummy variables  g 
y  z  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsxp.k . . . 4  |-  ( ph  ->  K  e.  ( ~P A  i^i  Fin )
)
2 elfpw 7601 . . . . 5  |-  ( K  e.  ( ~P A  i^i  Fin )  <->  ( K  C_  A  /\  K  e. 
Fin ) )
32simprbi 461 . . . 4  |-  ( K  e.  ( ~P A  i^i  Fin )  ->  K  e.  Fin )
41, 3syl 16 . . 3  |-  ( ph  ->  K  e.  Fin )
52simplbi 457 . . . . . . 7  |-  ( K  e.  ( ~P A  i^i  Fin )  ->  K  C_  A )
61, 5syl 16 . . . . . 6  |-  ( ph  ->  K  C_  A )
76sselda 3344 . . . . 5  |-  ( (
ph  /\  j  e.  K )  ->  j  e.  A )
8 tsmsxp.b . . . . . 6  |-  B  =  ( Base `  G
)
9 tsmsxp.j . . . . . 6  |-  J  =  ( TopOpen `  G )
10 eqid 2433 . . . . . 6  |-  ( ~P C  i^i  Fin )  =  ( ~P C  i^i  Fin )
11 tsmsxp.g . . . . . . 7  |-  ( ph  ->  G  e. CMnd )
1211adantr 462 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  G  e. CMnd )
13 tsmsxp.2 . . . . . . . 8  |-  ( ph  ->  G  e.  TopGrp )
14 tgptps 19493 . . . . . . . 8  |-  ( G  e.  TopGrp  ->  G  e.  TopSp )
1513, 14syl 16 . . . . . . 7  |-  ( ph  ->  G  e.  TopSp )
1615adantr 462 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  TopSp )
17 tsmsxp.c . . . . . . 7  |-  ( ph  ->  C  e.  W )
1817adantr 462 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  C  e.  W )
19 tsmsxp.f . . . . . . . . 9  |-  ( ph  ->  F : ( A  X.  C ) --> B )
20 fovrn 6222 . . . . . . . . 9  |-  ( ( F : ( A  X.  C ) --> B  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
2119, 20syl3an1 1244 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
22213expa 1180 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  C )  ->  (
j F k )  e.  B )
23 eqid 2433 . . . . . . 7  |-  ( k  e.  C  |->  ( j F k ) )  =  ( k  e.  C  |->  ( j F k ) )
2422, 23fmptd 5855 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  (
k  e.  C  |->  ( j F k ) ) : C --> B )
25 tsmsxp.1 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  ( G tsums  ( k  e.  C  |->  ( j F k ) ) ) )
26 df-ima 4840 . . . . . . . 8  |-  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
) " L )  =  ran  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
)  |`  L )
279, 8tgptopon 19495 . . . . . . . . . . . . 13  |-  ( G  e.  TopGrp  ->  J  e.  (TopOn `  B ) )
2813, 27syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  (TopOn `  B ) )
29 tsmsxp.l . . . . . . . . . . . 12  |-  ( ph  ->  L  e.  J )
30 toponss 18376 . . . . . . . . . . . 12  |-  ( ( J  e.  (TopOn `  B )  /\  L  e.  J )  ->  L  C_  B )
3128, 29, 30syl2anc 654 . . . . . . . . . . 11  |-  ( ph  ->  L  C_  B )
3231adantr 462 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  L  C_  B )
33 resmpt 5144 . . . . . . . . . 10  |-  ( L 
C_  B  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) )  |`  L )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
3432, 33syl 16 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) )  |`  L )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
3534rneqd 5054 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( ( g  e.  B  |->  ( ( H `
 j )  .-  g ) )  |`  L )  =  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) ) )
3626, 35syl5eq 2477 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) ) " L
)  =  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) )
37 tsmsxp.h . . . . . . . . . . . . 13  |-  ( ph  ->  H : A --> B )
3837ffvelrnda 5831 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  B )
39 tsmsxp.p . . . . . . . . . . . . 13  |-  .+  =  ( +g  `  G )
40 eqid 2433 . . . . . . . . . . . . 13  |-  ( invg `  G )  =  ( invg `  G )
41 tsmsxp.m . . . . . . . . . . . . 13  |-  .-  =  ( -g `  G )
428, 39, 40, 41grpsubval 15561 . . . . . . . . . . . 12  |-  ( ( ( H `  j
)  e.  B  /\  g  e.  B )  ->  ( ( H `  j )  .-  g
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
4338, 42sylan 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .+  ( ( invg `  G ) `  g
) ) )
4443mpteq2dva 4366 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
45 tgpgrp 19491 . . . . . . . . . . . . . 14  |-  ( G  e.  TopGrp  ->  G  e.  Grp )
4613, 45syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  G  e.  Grp )
4746adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  Grp )
488, 40grpinvcl 15563 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  g  e.  B )  ->  ( ( invg `  G ) `  g
)  e.  B )
4947, 48sylan 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( invg `  G ) `  g
)  e.  B )
508, 40grpinvf 15562 . . . . . . . . . . . . 13  |-  ( G  e.  Grp  ->  ( invg `  G ) : B --> B )
5147, 50syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G ) : B --> B )
5251feqmptd 5732 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G )  =  ( g  e.  B  |->  ( ( invg `  G ) `
 g ) ) )
53 eqidd 2434 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  =  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) ) )
54 oveq2 6088 . . . . . . . . . . 11  |-  ( y  =  ( ( invg `  G ) `
 g )  -> 
( ( H `  j )  .+  y
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
5549, 52, 53, 54fmptco 5863 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
5644, 55eqtr4d 2468 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( ( y  e.  B  |->  ( ( H `  j
)  .+  y )
)  o.  ( invg `  G ) ) )
5713adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  TopGrp )
589, 40grpinvhmeo 19499 . . . . . . . . . . 11  |-  ( G  e.  TopGrp  ->  ( invg `  G )  e.  ( J Homeo J ) )
5957, 58syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G )  e.  ( J Homeo J ) )
60 eqid 2433 . . . . . . . . . . . 12  |-  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) )  =  ( y  e.  B  |->  ( ( H `
 j )  .+  y ) )
6160, 8, 39, 9tgplacthmeo 19516 . . . . . . . . . . 11  |-  ( ( G  e.  TopGrp  /\  ( H `  j )  e.  B )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
6257, 38, 61syl2anc 654 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
63 hmeoco 19187 . . . . . . . . . 10  |-  ( ( ( invg `  G )  e.  ( J Homeo J )  /\  ( y  e.  B  |->  ( ( H `  j )  .+  y
) )  e.  ( J Homeo J ) )  ->  ( ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) )  o.  ( invg `  G ) )  e.  ( J Homeo J ) )
6459, 62, 63syl2anc 654 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  e.  ( J
Homeo J ) )
6556, 64eqeltrd 2507 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  e.  ( J
Homeo J ) )
6629adantr 462 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  L  e.  J )
67 hmeoima 19180 . . . . . . . 8  |-  ( ( ( g  e.  B  |->  ( ( H `  j )  .-  g
) )  e.  ( J Homeo J )  /\  L  e.  J )  ->  ( ( g  e.  B  |->  ( ( H `
 j )  .-  g ) ) " L )  e.  J
)
6865, 66, 67syl2anc 654 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) ) " L
)  e.  J )
6936, 68eqeltrrd 2508 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) )  e.  J
)
70 tsmsxp.z . . . . . . . . 9  |-  .0.  =  ( 0g `  G )
718, 70, 41grpsubid1 15591 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  ( H `  j )  e.  B )  -> 
( ( H `  j )  .-  .0.  )  =  ( H `  j ) )
7247, 38, 71syl2anc 654 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  =  ( H `  j ) )
73 tsmsxp.3 . . . . . . . . 9  |-  ( ph  ->  .0.  e.  L )
7473adantr 462 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  .0.  e.  L )
75 ovex 6105 . . . . . . . 8  |-  ( ( H `  j ) 
.-  .0.  )  e.  _V
76 eqid 2433 . . . . . . . . 9  |-  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )
77 oveq2 6088 . . . . . . . . 9  |-  ( g  =  .0.  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .-  .0.  ) )
7876, 77elrnmpt1s 5074 . . . . . . . 8  |-  ( (  .0.  e.  L  /\  ( ( H `  j )  .-  .0.  )  e.  _V )  ->  ( ( H `  j )  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) ) )
7974, 75, 78sylancl 655 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
8072, 79eqeltrrd 2508 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
818, 9, 10, 12, 16, 18, 24, 25, 69, 80tsmsi 19546 . . . . 5  |-  ( (
ph  /\  j  e.  A )  ->  E. y  e.  ( ~P C  i^i  Fin ) A. z  e.  ( ~P C  i^i  Fin ) ( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) ) )
827, 81syldan 467 . . . 4  |-  ( (
ph  /\  j  e.  K )  ->  E. y  e.  ( ~P C  i^i  Fin ) A. z  e.  ( ~P C  i^i  Fin ) ( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) ) )
8382ralrimiva 2789 . . 3  |-  ( ph  ->  A. j  e.  K  E. y  e.  ( ~P C  i^i  Fin ) A. z  e.  ( ~P C  i^i  Fin )
( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )
84 sseq1 3365 . . . . . 6  |-  ( y  =  ( f `  j )  ->  (
y  C_  z  <->  ( f `  j )  C_  z
) )
8584imbi1d 317 . . . . 5  |-  ( y  =  ( f `  j )  ->  (
( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  <-> 
( ( f `  j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )
8685ralbidv 2725 . . . 4  |-  ( y  =  ( f `  j )  ->  ( A. z  e.  ( ~P C  i^i  Fin )
( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  <->  A. z  e.  ( ~P C  i^i  Fin )
( ( f `  j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )
8786ac6sfi 7544 . . 3  |-  ( ( K  e.  Fin  /\  A. j  e.  K  E. y  e.  ( ~P C  i^i  Fin ) A. z  e.  ( ~P C  i^i  Fin ) ( y  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )  ->  E. f
( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `
 j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) ) ) )
884, 83, 87syl2anc 654 . 2  |-  ( ph  ->  E. f ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin )
( ( f `  j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )
89 frn 5553 . . . . . . . . 9  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  ran  f  C_  ( ~P C  i^i  Fin )
)
9089adantl 463 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ( ~P C  i^i  Fin ) )
91 inss1 3558 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
~P C
9290, 91syl6ss 3356 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ~P C )
93 sspwuni 4244 . . . . . . 7  |-  ( ran  f  C_  ~P C  <->  U.
ran  f  C_  C
)
9492, 93sylib 196 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  U. ran  f  C_  C )
95 tsmsxp.d . . . . . . . . 9  |-  ( ph  ->  D  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
96 elfpw 7601 . . . . . . . . . 10  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  <->  ( D  C_  ( A  X.  C
)  /\  D  e.  Fin ) )
9796simplbi 457 . . . . . . . . 9  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  C_  ( A  X.  C
) )
98 rnss 5055 . . . . . . . . 9  |-  ( D 
C_  ( A  X.  C )  ->  ran  D 
C_  ran  ( A  X.  C ) )
9995, 97, 983syl 20 . . . . . . . 8  |-  ( ph  ->  ran  D  C_  ran  ( A  X.  C
) )
100 rnxpss 5258 . . . . . . . 8  |-  ran  ( A  X.  C )  C_  C
10199, 100syl6ss 3356 . . . . . . 7  |-  ( ph  ->  ran  D  C_  C
)
102101adantr 462 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D 
C_  C )
10394, 102unssd 3520 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  C_  C )
1044adantr 462 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  K  e.  Fin )
105 ffn 5547 . . . . . . . . . 10  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  f  Fn  K )
106105adantl 463 . . . . . . . . 9  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  f  Fn  K )
107 dffn4 5614 . . . . . . . . 9  |-  ( f  Fn  K  <->  f : K -onto-> ran  f )
108106, 107sylib 196 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  f : K -onto-> ran  f )
109 fofi 7585 . . . . . . . 8  |-  ( ( K  e.  Fin  /\  f : K -onto-> ran  f
)  ->  ran  f  e. 
Fin )
110104, 108, 109syl2anc 654 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  e.  Fin )
111 inss2 3559 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
Fin
11290, 111syl6ss 3356 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  Fin )
113 unifi 7588 . . . . . . 7  |-  ( ( ran  f  e.  Fin  /\ 
ran  f  C_  Fin )  ->  U. ran  f  e. 
Fin )
114110, 112, 113syl2anc 654 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  U. ran  f  e.  Fin )
11596simprbi 461 . . . . . . . 8  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  e.  Fin )
116 rnfi 7584 . . . . . . . 8  |-  ( D  e.  Fin  ->  ran  D  e.  Fin )
11795, 115, 1163syl 20 . . . . . . 7  |-  ( ph  ->  ran  D  e.  Fin )
118117adantr 462 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D  e.  Fin )
119 unfi 7567 . . . . . 6  |-  ( ( U. ran  f  e. 
Fin  /\  ran  D  e. 
Fin )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
120114, 118, 119syl2anc 654 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
121 elfpw 7601 . . . . 5  |-  ( ( U. ran  f  u. 
ran  D )  e.  ( ~P C  i^i  Fin )  <->  ( ( U. ran  f  u.  ran  D )  C_  C  /\  ( U. ran  f  u. 
ran  D )  e. 
Fin ) )
122103, 120, 121sylanbrc 657 . . . 4  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin )
)
123122adantrr 709 . . 3  |-  ( (
ph  /\  ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )  ->  ( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin )
)
124 ssun2 3508 . . . 4  |-  ran  D  C_  ( U. ran  f  u.  ran  D )
125124a1i 11 . . 3  |-  ( (
ph  /\  ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )  ->  ran  D 
C_  ( U. ran  f  u.  ran  D ) )
126122adantlr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin ) )
127 fvssunirn 5701 . . . . . . . . . . . . . 14  |-  ( f `
 j )  C_  U.
ran  f
128 ssun1 3507 . . . . . . . . . . . . . 14  |-  U. ran  f  C_  ( U. ran  f  u.  ran  D )
129127, 128sstri 3353 . . . . . . . . . . . . 13  |-  ( f `
 j )  C_  ( U. ran  f  u. 
ran  D )
130 id 22 . . . . . . . . . . . . 13  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  z  =  ( U. ran  f  u. 
ran  D ) )
131129, 130syl5sseqr 3393 . . . . . . . . . . . 12  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( f `  j )  C_  z
)
132 pm5.5 336 . . . . . . . . . . . 12  |-  ( ( f `  j ) 
C_  z  ->  (
( ( f `  j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  <-> 
( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )
133131, 132syl 16 . . . . . . . . . . 11  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( ( ( f `  j ) 
C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  <-> 
( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )
134 reseq2 5092 . . . . . . . . . . . . 13  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( ( k  e.  C  |->  ( j F k ) )  |`  z )  =  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) ) )
135134oveq2d 6096 . . . . . . . . . . . 12  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  =  ( G 
gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) ) ) )
136135eleq1d 2499 . . . . . . . . . . 11  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( ( G 
gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )  <->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )
137133, 136bitrd 253 . . . . . . . . . 10  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( ( ( f `  j ) 
C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  <-> 
( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) ) )  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) ) )
138137rspcv 3058 . . . . . . . . 9  |-  ( ( U. ran  f  u. 
ran  D )  e.  ( ~P C  i^i  Fin )  ->  ( A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) )
139126, 138syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( A. z  e.  ( ~P C  i^i  Fin ) ( ( f `
 j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) )  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) ) )  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) ) )
14011ad2antrr 718 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  G  e. CMnd )
141 cmnmnd 16272 . . . . . . . . . . . . 13  |-  ( G  e. CMnd  ->  G  e.  Mnd )
142140, 141syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  G  e.  Mnd )
143 simplr 747 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  K )
144120adantlr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  e. 
Fin )
145103adantlr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  C_  C )
146145sselda 3344 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  ( U. ran  f  u. 
ran  D ) )  ->  k  e.  C
)
14719adantr 462 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  K )  ->  F : ( A  X.  C ) --> B )
148147, 7jca 529 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  K )  ->  ( F : ( A  X.  C ) --> B  /\  j  e.  A )
)
149203expa 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : ( A  X.  C ) --> B  /\  j  e.  A )  /\  k  e.  C )  ->  (
j F k )  e.  B )
150148, 149sylan 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  k  e.  C )  ->  (
j F k )  e.  B )
151150adantlr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  C )  ->  (
j F k )  e.  B )
152146, 151syldan 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  ( U. ran  f  u. 
ran  D ) )  ->  ( j F k )  e.  B
)
153 eqid 2433 . . . . . . . . . . . . . 14  |-  ( k  e.  ( U. ran  f  u.  ran  D ) 
|->  ( j F k ) )  =  ( k  e.  ( U. ran  f  u.  ran  D )  |->  ( j F k ) )
154152, 153fmptd 5855 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) : ( U. ran  f  u.  ran  D ) --> B )
155 ovex 6105 . . . . . . . . . . . . . . 15  |-  ( j F k )  e. 
_V
156155a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  ( U. ran  f  u. 
ran  D ) )  ->  ( j F k )  e.  _V )
157 fvex 5689 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  G )  e. 
_V
15870, 157eqeltri 2503 . . . . . . . . . . . . . . 15  |-  .0.  e.  _V
159158a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  .0.  e.  _V )
160153, 144, 156, 159fsuppmptdm 7619 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) finSupp  .0.  )
1618, 70, 140, 144, 154, 160gsumcl 16377 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( G  gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) )  e.  B
)
162 elsn 3879 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { j }  <-> 
y  =  j )
163 ovres 6219 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  { j }  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  ( y ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) k )  =  ( y F k ) )
164162, 163sylanbr 470 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  j  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  (
y ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) k )  =  ( y F k ) )
165 oveq1 6087 . . . . . . . . . . . . . . . . 17  |-  ( y  =  j  ->  (
y F k )  =  ( j F k ) )
166165adantr 462 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  j  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  (
y F k )  =  ( j F k ) )
167164, 166eqtrd 2465 . . . . . . . . . . . . . . 15  |-  ( ( y  =  j  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  (
y ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) k )  =  ( j F k ) )
168167mpteq2dva 4366 . . . . . . . . . . . . . 14  |-  ( y  =  j  ->  (
k  e.  ( U. ran  f  u.  ran  D )  |->  ( y ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) k ) )  =  ( k  e.  ( U. ran  f  u.  ran  D )  |->  ( j F k ) ) )
169168oveq2d 6096 . . . . . . . . . . . . 13  |-  ( y  =  j  ->  ( G  gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( y ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) k ) ) )  =  ( G 
gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) ) )
1708, 169gsumsn 16425 . . . . . . . . . . . 12  |-  ( ( G  e.  Mnd  /\  j  e.  K  /\  ( G  gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) )  e.  B
)  ->  ( G  gsumg  ( y  e.  { j }  |->  ( G  gsumg  ( k  e.  ( U. ran  f  u.  ran  D ) 
|->  ( y ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) ) k ) ) ) ) )  =  ( G  gsumg  ( k  e.  ( U. ran  f  u.  ran  D ) 
|->  ( j F k ) ) ) )
171142, 143, 161, 170syl3anc 1211 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( G  gsumg  ( y  e.  {
j }  |->  ( G 
gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( y ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) k ) ) ) ) )  =  ( G  gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) ) )
172 snfi 7378 . . . . . . . . . . . . 13  |-  { j }  e.  Fin
173172a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  e.  Fin )
17419ad2antrr 718 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  F : ( A  X.  C ) --> B )
1757adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  A )
176175snssd 4006 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  C_  A )
177 xpss12 4932 . . . . . . . . . . . . . 14  |-  ( ( { j }  C_  A  /\  ( U. ran  f  u.  ran  D ) 
C_  C )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  C_  ( A  X.  C ) )
178176, 145, 177syl2anc 654 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  C_  ( A  X.  C ) )
179 fssres 5566 . . . . . . . . . . . . 13  |-  ( ( F : ( A  X.  C ) --> B  /\  ( { j }  X.  ( U. ran  f  u.  ran  D ) )  C_  ( A  X.  C ) )  ->  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) : ( { j }  X.  ( U. ran  f  u.  ran  D ) ) --> B )
180174, 178, 179syl2anc 654 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) : ( { j }  X.  ( U. ran  f  u.  ran  D ) ) --> B )
181 xpfi 7571 . . . . . . . . . . . . . 14  |-  ( ( { j }  e.  Fin  /\  ( U. ran  f  u.  ran  D )  e.  Fin )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  e.  Fin )
182172, 144, 181sylancr 656 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  e.  Fin )
183180, 182, 159fdmfifsupp 7618 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) finSupp  .0.  )
1848, 70, 140, 173, 144, 180, 183gsumxp 16442 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  =  ( G  gsumg  ( y  e.  {
j }  |->  ( G 
gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( y ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) k ) ) ) ) ) )
185 resmpt 5144 . . . . . . . . . . . . 13  |-  ( ( U. ran  f  u. 
ran  D )  C_  C  ->  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) )  =  ( k  e.  ( U. ran  f  u.  ran  D )  |->  ( j F k ) ) )
186145, 185syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) )  =  ( k  e.  ( U. ran  f  u.  ran  D )  |->  ( j F k ) ) )
187186oveq2d 6096 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) ) )  =  ( G 
gsumg  ( k  e.  ( U. ran  f  u. 
ran  D )  |->  ( j F k ) ) ) )
188171, 184, 1873eqtr4rd 2476 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u. 
ran  D ) ) )  =  ( G 
gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )
189188eleq1d 2499 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )  <->  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) )  e.  ran  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) ) ) )
190 ovex 6105 . . . . . . . . . . 11  |-  ( ( H `  j ) 
.-  g )  e. 
_V
19176, 190elrnmpti 5077 . . . . . . . . . 10  |-  ( ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  e.  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) )  <->  E. g  e.  L  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) )  =  ( ( H `
 j )  .-  g ) )
192 isabl 16261 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
19346, 11, 192sylanbrc 657 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  Abel )
194193ad3antrrr 722 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  G  e.  Abel )
1957, 38syldan 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  K )  ->  ( H `  j )  e.  B )
196195ad2antrr 718 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  ( H `  j )  e.  B )
19731ad2antrr 718 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  L  C_  B )
198197sselda 3344 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  B )
1998, 41, 194, 196, 198ablnncan 16290 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  =  g )
200 simpr 458 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  L )
201199, 200eqeltrd 2507 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  e.  L )
202 oveq2 6088 . . . . . . . . . . . . 13  |-  ( ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  =  ( ( H `  j
)  .-  g )  ->  ( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  =  ( ( H `  j )  .-  (
( H `  j
)  .-  g )
) )
203202eleq1d 2499 . . . . . . . . . . . 12  |-  ( ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  =  ( ( H `  j
)  .-  g )  ->  ( ( ( H `
 j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L  <->  ( ( H `
 j )  .-  ( ( H `  j )  .-  g
) )  e.  L
) )
204201, 203syl5ibrcom 222 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  =  ( ( H `  j
)  .-  g )  ->  ( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
205204rexlimdva 2831 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( E. g  e.  L  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) ) )  =  ( ( H `  j )  .-  g
)  ->  ( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
206191, 205syl5bi 217 . . . . . . . . 9  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )  -> 
( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
207189, 206sylbid 215 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  ( U. ran  f  u.  ran  D ) ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )  -> 
( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
208139, 207syld 44 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( A. z  e.  ( ~P C  i^i  Fin ) ( ( f `
 j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) )  ->  (
( H `  j
)  .-  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )  e.  L ) )
209208an32s 795 . . . . . 6  |-  ( ( ( ph  /\  f : K --> ( ~P C  i^i  Fin ) )  /\  j  e.  K )  ->  ( A. z  e.  ( ~P C  i^i  Fin ) ( ( f `
 j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z )
)  e.  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) )  ->  (
( H `  j
)  .-  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )  e.  L ) )
210209ralimdva 2784 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin )
( ( f `  j )  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )  ->  A. j  e.  K  ( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
211210impr 614 . . . 4  |-  ( (
ph  /\  ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )  ->  A. j  e.  K  ( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L )
212 fveq2 5679 . . . . . . 7  |-  ( j  =  x  ->  ( H `  j )  =  ( H `  x ) )
213 sneq 3875 . . . . . . . . . 10  |-  ( j  =  x  ->  { j }  =  { x } )
214213xpeq1d 4850 . . . . . . . . 9  |-  ( j  =  x  ->  ( { j }  X.  ( U. ran  f  u. 
ran  D ) )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
215214reseq2d 5097 . . . . . . . 8  |-  ( j  =  x  ->  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
216215oveq2d 6096 . . . . . . 7  |-  ( j  =  x  ->  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) )  =  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )
217212, 216oveq12d 6098 . . . . . 6  |-  ( j  =  x  ->  (
( H `  j
)  .-  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )  =  ( ( H `  x ) 
.-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) ) ) ) )
218217eleq1d 2499 . . . . 5  |-  ( j  =  x  ->  (
( ( H `  j )  .-  ( G  gsumg  ( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L  <->  ( ( H `
 x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
219218cbvralv 2937 . . . 4  |-  ( A. j  e.  K  (
( H `  j
)  .-  ( G  gsumg  ( F  |`  ( {
j }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )  e.  L  <->  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L )
220211, 219sylib 196 . . 3  |-  ( (
ph  /\  ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )  ->  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L )
221 sseq2 3366 . . . . 5  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ran  D  C_  n  <->  ran  D  C_  ( U. ran  f  u.  ran  D ) ) )
222 xpeq2 4842 . . . . . . . . . 10  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( { x }  X.  n )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
223222reseq2d 5097 . . . . . . . . 9  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( F  |`  ( { x }  X.  n ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
224223oveq2d 6096 . . . . . . . 8  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) )  =  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) ) ) )
225224oveq2d 6096 . . . . . . 7  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ( H `
 x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  =  ( ( H `  x ) 
.-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) ) ) ) )
226225eleq1d 2499 . . . . . 6  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ( ( H `  x ) 
.-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L  <->  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
227226ralbidv 2725 . . . . 5  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L  <->  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )
228221, 227anbi12d 703 . . . 4  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ( ran 
D  C_  n  /\  A. x  e.  K  ( ( H `  x
)  .-  ( G  gsumg  ( F  |`  ( {
x }  X.  n
) ) ) )  e.  L )  <->  ( ran  D 
C_  ( U. ran  f  u.  ran  D )  /\  A. x  e.  K  ( ( H `
 x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) ) )
229228rspcev 3062 . . 3  |-  ( ( ( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin )  /\  ( ran 
D  C_  ( U. ran  f  u.  ran  D )  /\  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) ) )  e.  L ) )  ->  E. n  e.  ( ~P C  i^i  Fin )
( ran  D  C_  n  /\  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L ) )
230123, 125, 220, 229syl12anc 1209 . 2  |-  ( (
ph  /\  ( f : K --> ( ~P C  i^i  Fin )  /\  A. j  e.  K  A. z  e.  ( ~P C  i^i  Fin ) ( ( f `  j
)  C_  z  ->  ( G  gsumg  ( ( k  e.  C  |->  ( j F k ) )  |`  z ) )  e. 
ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) ) ) )  ->  E. n  e.  ( ~P C  i^i  Fin ) ( ran  D  C_  n  /\  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L ) )
23188, 230exlimddv 1691 1  |-  ( ph  ->  E. n  e.  ( ~P C  i^i  Fin ) ( ran  D  C_  n  /\  A. x  e.  K  ( ( H `  x )  .-  ( G  gsumg  ( F  |`  ( { x }  X.  n ) ) ) )  e.  L ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362   E.wex 1589    e. wcel 1755   A.wral 2705   E.wrex 2706   _Vcvv 2962    u. cun 3314    i^i cin 3315    C_ wss 3316   ~Pcpw 3848   {csn 3865   U.cuni 4079    e. cmpt 4338    X. cxp 4825   dom cdm 4827   ran crn 4828    |` cres 4829   "cima 4830    o. ccom 4831    Fn wfn 5401   -->wf 5402   -onto->wfo 5404   ` cfv 5406  (class class class)co 6080   Fincfn 7298   Basecbs 14157   +g cplusg 14221   TopOpenctopn 14343   0gc0g 14361    gsumg cgsu 14362   Mndcmnd 15392   Grpcgrp 15393   invgcminusg 15394   -gcsg 15396  CMndccmn 16257   Abelcabel 16258  TopOnctopon 18341   TopSpctps 18343   Homeochmeo 19168   TopGrpctgp 19484   tsums ctsu 19538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-map 7204  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-oi 7712  df-card 8097  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-2 10368  df-n0 10568  df-z 10635  df-uz 10850  df-fz 11425  df-fzo 11533  df-seq 11791  df-hash 12088  df-ndx 14160  df-slot 14161  df-base 14162  df-sets 14163  df-ress 14164  df-plusg 14234  df-0g 14363  df-gsum 14364  df-topgen 14365  df-mre 14507  df-mrc 14508  df-acs 14510  df-mnd 15398  df-plusf 15399  df-submnd 15448  df-grp 15525  df-minusg 15526  df-sbg 15527  df-mulg 15528  df-cntz 15815  df-cmn 16259  df-abl 16260  df-fbas 17658  df-fg 17659  df-top 18345  df-bases 18347  df-topon 18348  df-topsp 18349  df-ntr 18466  df-nei 18544  df-cn 18673  df-cnp 18674  df-tx 18977  df-hmeo 19170  df-fil 19261  df-fm 19353  df-flim 19354  df-flf 19355  df-tmd 19485  df-tgp 19486  df-tsms 19539
This theorem is referenced by:  tsmsxp  19571
  Copyright terms: Public domain W3C validator