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

Theorem tsmsxplem1 19749
Description: Lemma for tsmsxp 19751. (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 7634 . . . . 5  |-  ( K  e.  ( ~P A  i^i  Fin )  <->  ( K  C_  A  /\  K  e. 
Fin ) )
32simprbi 464 . . . 4  |-  ( K  e.  ( ~P A  i^i  Fin )  ->  K  e.  Fin )
41, 3syl 16 . . 3  |-  ( ph  ->  K  e.  Fin )
52simplbi 460 . . . . . . 7  |-  ( K  e.  ( ~P A  i^i  Fin )  ->  K  C_  A )
61, 5syl 16 . . . . . 6  |-  ( ph  ->  K  C_  A )
76sselda 3377 . . . . 5  |-  ( (
ph  /\  j  e.  K )  ->  j  e.  A )
8 tsmsxp.b . . . . . 6  |-  B  =  ( Base `  G
)
9 tsmsxp.j . . . . . 6  |-  J  =  ( TopOpen `  G )
10 eqid 2443 . . . . . 6  |-  ( ~P C  i^i  Fin )  =  ( ~P C  i^i  Fin )
11 tsmsxp.g . . . . . . 7  |-  ( ph  ->  G  e. CMnd )
1211adantr 465 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  G  e. CMnd )
13 tsmsxp.2 . . . . . . . 8  |-  ( ph  ->  G  e.  TopGrp )
14 tgptps 19673 . . . . . . . 8  |-  ( G  e.  TopGrp  ->  G  e.  TopSp )
1513, 14syl 16 . . . . . . 7  |-  ( ph  ->  G  e.  TopSp )
1615adantr 465 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  TopSp )
17 tsmsxp.c . . . . . . 7  |-  ( ph  ->  C  e.  W )
1817adantr 465 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  C  e.  W )
19 tsmsxp.f . . . . . . . . 9  |-  ( ph  ->  F : ( A  X.  C ) --> B )
20 fovrn 6254 . . . . . . . . 9  |-  ( ( F : ( A  X.  C ) --> B  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
2119, 20syl3an1 1251 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
22213expa 1187 . . . . . . 7  |-  ( ( ( ph  /\  j  e.  A )  /\  k  e.  C )  ->  (
j F k )  e.  B )
23 eqid 2443 . . . . . . 7  |-  ( k  e.  C  |->  ( j F k ) )  =  ( k  e.  C  |->  ( j F k ) )
2422, 23fmptd 5888 . . . . . 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 4874 . . . . . . . 8  |-  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
) " L )  =  ran  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
)  |`  L )
279, 8tgptopon 19675 . . . . . . . . . . . . 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 18556 . . . . . . . . . . . 12  |-  ( ( J  e.  (TopOn `  B )  /\  L  e.  J )  ->  L  C_  B )
3128, 29, 30syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  L  C_  B )
3231adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  L  C_  B )
33 resmpt 5177 . . . . . . . . . 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 5088 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( ( g  e.  B  |->  ( ( H `
 j )  .-  g ) )  |`  L )  =  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) ) )
3626, 35syl5eq 2487 . . . . . . 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 5864 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  B )
39 tsmsxp.p . . . . . . . . . . . . 13  |-  .+  =  ( +g  `  G )
40 eqid 2443 . . . . . . . . . . . . 13  |-  ( invg `  G )  =  ( invg `  G )
41 tsmsxp.m . . . . . . . . . . . . 13  |-  .-  =  ( -g `  G )
428, 39, 40, 41grpsubval 15602 . . . . . . . . . . . 12  |-  ( ( ( H `  j
)  e.  B  /\  g  e.  B )  ->  ( ( H `  j )  .-  g
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
4338, 42sylan 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .+  ( ( invg `  G ) `  g
) ) )
4443mpteq2dva 4399 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
45 tgpgrp 19671 . . . . . . . . . . . . . 14  |-  ( G  e.  TopGrp  ->  G  e.  Grp )
4613, 45syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  G  e.  Grp )
4746adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  Grp )
488, 40grpinvcl 15604 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  g  e.  B )  ->  ( ( invg `  G ) `  g
)  e.  B )
4947, 48sylan 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( invg `  G ) `  g
)  e.  B )
508, 40grpinvf 15603 . . . . . . . . . . . . 13  |-  ( G  e.  Grp  ->  ( invg `  G ) : B --> B )
5147, 50syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G ) : B --> B )
5251feqmptd 5765 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G )  =  ( g  e.  B  |->  ( ( invg `  G ) `
 g ) ) )
53 eqidd 2444 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  =  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) ) )
54 oveq2 6120 . . . . . . . . . . 11  |-  ( y  =  ( ( invg `  G ) `
 g )  -> 
( ( H `  j )  .+  y
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
5549, 52, 53, 54fmptco 5897 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
5644, 55eqtr4d 2478 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( ( y  e.  B  |->  ( ( H `  j
)  .+  y )
)  o.  ( invg `  G ) ) )
5713adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  TopGrp )
589, 40grpinvhmeo 19679 . . . . . . . . . . 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 2443 . . . . . . . . . . . 12  |-  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) )  =  ( y  e.  B  |->  ( ( H `
 j )  .+  y ) )
6160, 8, 39, 9tgplacthmeo 19696 . . . . . . . . . . 11  |-  ( ( G  e.  TopGrp  /\  ( H `  j )  e.  B )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
6257, 38, 61syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
63 hmeoco 19367 . . . . . . . . . 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 661 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  e.  ( J
Homeo J ) )
6556, 64eqeltrd 2517 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  e.  ( J
Homeo J ) )
6629adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  L  e.  J )
67 hmeoima 19360 . . . . . . . 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 661 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) ) " L
)  e.  J )
6936, 68eqeltrrd 2518 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) )  e.  J
)
70 tsmsxp.z . . . . . . . . 9  |-  .0.  =  ( 0g `  G )
718, 70, 41grpsubid1 15632 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  ( H `  j )  e.  B )  -> 
( ( H `  j )  .-  .0.  )  =  ( H `  j ) )
7247, 38, 71syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  =  ( H `  j ) )
73 tsmsxp.3 . . . . . . . . 9  |-  ( ph  ->  .0.  e.  L )
7473adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  .0.  e.  L )
75 ovex 6137 . . . . . . . 8  |-  ( ( H `  j ) 
.-  .0.  )  e.  _V
76 eqid 2443 . . . . . . . . 9  |-  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )
77 oveq2 6120 . . . . . . . . 9  |-  ( g  =  .0.  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .-  .0.  ) )
7876, 77elrnmpt1s 5108 . . . . . . . 8  |-  ( (  .0.  e.  L  /\  ( ( H `  j )  .-  .0.  )  e.  _V )  ->  ( ( H `  j )  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) ) )
7974, 75, 78sylancl 662 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
8072, 79eqeltrrd 2518 . . . . . 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 19726 . . . . 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 470 . . . 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 2820 . . 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 3398 . . . . . 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 2756 . . . 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 7577 . . 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 661 . 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 5586 . . . . . . . . 9  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  ran  f  C_  ( ~P C  i^i  Fin )
)
9089adantl 466 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ( ~P C  i^i  Fin ) )
91 inss1 3591 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
~P C
9290, 91syl6ss 3389 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ~P C )
93 sspwuni 4277 . . . . . . 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 7634 . . . . . . . . . 10  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  <->  ( D  C_  ( A  X.  C
)  /\  D  e.  Fin ) )
9796simplbi 460 . . . . . . . . 9  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  C_  ( A  X.  C
) )
98 rnss 5089 . . . . . . . . 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 5291 . . . . . . . 8  |-  ran  ( A  X.  C )  C_  C
10199, 100syl6ss 3389 . . . . . . 7  |-  ( ph  ->  ran  D  C_  C
)
102101adantr 465 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D 
C_  C )
10394, 102unssd 3553 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  C_  C )
1044adantr 465 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  K  e.  Fin )
105 ffn 5580 . . . . . . . . . 10  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  f  Fn  K )
106105adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  f  Fn  K )
107 dffn4 5647 . . . . . . . . 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 7618 . . . . . . . 8  |-  ( ( K  e.  Fin  /\  f : K -onto-> ran  f
)  ->  ran  f  e. 
Fin )
110104, 108, 109syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  e.  Fin )
111 inss2 3592 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
Fin
11290, 111syl6ss 3389 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  Fin )
113 unifi 7621 . . . . . . 7  |-  ( ( ran  f  e.  Fin  /\ 
ran  f  C_  Fin )  ->  U. ran  f  e. 
Fin )
114110, 112, 113syl2anc 661 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  U. ran  f  e.  Fin )
11596simprbi 464 . . . . . . . 8  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  e.  Fin )
116 rnfi 7617 . . . . . . . 8  |-  ( D  e.  Fin  ->  ran  D  e.  Fin )
11795, 115, 1163syl 20 . . . . . . 7  |-  ( ph  ->  ran  D  e.  Fin )
118117adantr 465 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D  e.  Fin )
119 unfi 7600 . . . . . 6  |-  ( ( U. ran  f  e. 
Fin  /\  ran  D  e. 
Fin )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
120114, 118, 119syl2anc 661 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
121 elfpw 7634 . . . . 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 664 . . . 4  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin )
)
123122adantrr 716 . . 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 3541 . . . 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 714 . . . . . . . . 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 5734 . . . . . . . . . . . . . 14  |-  ( f `
 j )  C_  U.
ran  f
128 ssun1 3540 . . . . . . . . . . . . . 14  |-  U. ran  f  C_  ( U. ran  f  u.  ran  D )
129127, 128sstri 3386 . . . . . . . . . . . . 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 3426 . . . . . . . . . . . 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 5126 . . . . . . . . . . . . 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 6128 . . . . . . . . . . . 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 2509 . . . . . . . . . . 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 3090 . . . . . . . . 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 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  G  e. CMnd )
141 cmnmnd 16313 . . . . . . . . . . . . 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 754 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  K )
144120adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  e. 
Fin )
145103adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  C_  C )
146145sselda 3377 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  ( U. ran  f  u. 
ran  D ) )  ->  k  e.  C
)
14719adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  K )  ->  F : ( A  X.  C ) --> B )
148147, 7jca 532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  K )  ->  ( F : ( A  X.  C ) --> B  /\  j  e.  A )
)
149203expa 1187 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : ( A  X.  C ) --> B  /\  j  e.  A )  /\  k  e.  C )  ->  (
j F k )  e.  B )
150148, 149sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  k  e.  C )  ->  (
j F k )  e.  B )
151150adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  C )  ->  (
j F k )  e.  B )
152146, 151syldan 470 . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . 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 5888 . . . . . . . . . . . . 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 6137 . . . . . . . . . . . . . . 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 5722 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  G )  e. 
_V
15870, 157eqeltri 2513 . . . . . . . . . . . . . . 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 7652 . . . . . . . . . . . . 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 16418 . . . . . . . . . . . 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 3912 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { j }  <-> 
y  =  j )
163 ovres 6251 . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . 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 6119 . . . . . . . . . . . . . . . . 17  |-  ( y  =  j  ->  (
y F k )  =  ( j F k ) )
166165adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  j  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  (
y F k )  =  ( j F k ) )
167164, 166eqtrd 2475 . . . . . . . . . . . . . . 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 4399 . . . . . . . . . . . . . 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 6128 . . . . . . . . . . . . 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 16471 . . . . . . . . . . . 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 1218 . . . . . . . . . . 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 7411 . . . . . . . . . . . . 13  |-  { j }  e.  Fin
173172a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  e.  Fin )
17419ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  F : ( A  X.  C ) --> B )
1757adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  A )
176175snssd 4039 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  C_  A )
177 xpss12 4966 . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . 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 5599 . . . . . . . . . . . . 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 661 . . . . . . . . . . . 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 7604 . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . 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 7651 . . . . . . . . . . . 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 16490 . . . . . . . . . . 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 5177 . . . . . . . . . . . . 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 6128 . . . . . . . . . . 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 2486 . . . . . . . . . 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 2509 . . . . . . . . 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 6137 . . . . . . . . . . 11  |-  ( ( H `  j ) 
.-  g )  e. 
_V
19176, 190elrnmpti 5111 . . . . . . . . . 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 16302 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
19346, 11, 192sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  Abel )
194193ad3antrrr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  G  e.  Abel )
1957, 38syldan 470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  K )  ->  ( H `  j )  e.  B )
196195ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  ( H `  j )  e.  B )
19731ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  L  C_  B )
198197sselda 3377 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  B )
1998, 41, 194, 196, 198ablnncan 16331 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  =  g )
200 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  L )
201199, 200eqeltrd 2517 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  e.  L )
202 oveq2 6120 . . . . . . . . . . . . 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 2509 . . . . . . . . . . . 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 2862 . . . . . . . . . 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 802 . . . . . 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 2815 . . . . 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 619 . . . 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 5712 . . . . . . 7  |-  ( j  =  x  ->  ( H `  j )  =  ( H `  x ) )
213 sneq 3908 . . . . . . . . . 10  |-  ( j  =  x  ->  { j }  =  { x } )
214213xpeq1d 4884 . . . . . . . . 9  |-  ( j  =  x  ->  ( { j }  X.  ( U. ran  f  u. 
ran  D ) )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
215214reseq2d 5131 . . . . . . . 8  |-  ( j  =  x  ->  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
216215oveq2d 6128 . . . . . . 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 6130 . . . . . 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 2509 . . . . 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 2968 . . . 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 3399 . . . . 5  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ran  D  C_  n  <->  ran  D  C_  ( U. ran  f  u.  ran  D ) ) )
222 xpeq2 4876 . . . . . . . . . 10  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( { x }  X.  n )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
223222reseq2d 5131 . . . . . . . . 9  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( F  |`  ( { x }  X.  n ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
224223oveq2d 6128 . . . . . . . 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 6128 . . . . . . 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 2509 . . . . . 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 2756 . . . . 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 710 . . . 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 3094 . . 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 1216 . 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 1692 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 1369   E.wex 1586    e. wcel 1756   A.wral 2736   E.wrex 2737   _Vcvv 2993    u. cun 3347    i^i cin 3348    C_ wss 3349   ~Pcpw 3881   {csn 3898   U.cuni 4112    e. cmpt 4371    X. cxp 4859   dom cdm 4861   ran crn 4862    |` cres 4863   "cima 4864    o. ccom 4865    Fn wfn 5434   -->wf 5435   -onto->wfo 5437   ` cfv 5439  (class class class)co 6112   Fincfn 7331   Basecbs 14195   +g cplusg 14259   TopOpenctopn 14381   0gc0g 14399    gsumg cgsu 14400   Mndcmnd 15430   Grpcgrp 15431   invgcminusg 15432   -gcsg 15434  CMndccmn 16298   Abelcabel 16299  TopOnctopon 18521   TopSpctps 18523   Homeochmeo 19348   TopGrpctgp 19664   tsums ctsu 19718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-iin 4195  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-of 6341  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-er 7122  df-map 7237  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-oi 7745  df-card 8130  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-nn 10344  df-2 10401  df-n0 10601  df-z 10668  df-uz 10883  df-fz 11459  df-fzo 11570  df-seq 11828  df-hash 12125  df-ndx 14198  df-slot 14199  df-base 14200  df-sets 14201  df-ress 14202  df-plusg 14272  df-0g 14401  df-gsum 14402  df-topgen 14403  df-mre 14545  df-mrc 14546  df-acs 14548  df-mnd 15436  df-plusf 15437  df-submnd 15486  df-grp 15566  df-minusg 15567  df-sbg 15568  df-mulg 15569  df-cntz 15856  df-cmn 16300  df-abl 16301  df-fbas 17836  df-fg 17837  df-top 18525  df-bases 18527  df-topon 18528  df-topsp 18529  df-ntr 18646  df-nei 18724  df-cn 18853  df-cnp 18854  df-tx 19157  df-hmeo 19350  df-fil 19441  df-fm 19533  df-flim 19534  df-flf 19535  df-tmd 19665  df-tgp 19666  df-tsms 19719
This theorem is referenced by:  tsmsxp  19751
  Copyright terms: Public domain W3C validator