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

Theorem tsmsxplem1 20633
Description: Lemma for tsmsxp 20635. (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 7824 . . . . 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 3489 . . . . 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 20557 . . . . . . . 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 6430 . . . . . . . . 9  |-  ( ( F : ( A  X.  C ) --> B  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
2119, 20syl3an1 1262 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A  /\  k  e.  C
)  ->  ( j F k )  e.  B )
22213expa 1197 . . . . . . 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 6040 . . . . . 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 5002 . . . . . . . 8  |-  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
) " L )  =  ran  ( ( g  e.  B  |->  ( ( H `  j
)  .-  g )
)  |`  L )
279, 8tgptopon 20559 . . . . . . . . . . . . 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 19408 . . . . . . . . . . . 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 )
3332resmptd 5315 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) )  |`  L )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
3433rneqd 5220 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( ( g  e.  B  |->  ( ( H `
 j )  .-  g ) )  |`  L )  =  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) ) )
3526, 34syl5eq 2496 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) ) " L
)  =  ran  (
g  e.  L  |->  ( ( H `  j
)  .-  g )
) )
36 tsmsxp.h . . . . . . . . . . . . 13  |-  ( ph  ->  H : A --> B )
3736ffvelrnda 6016 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  B )
38 tsmsxp.p . . . . . . . . . . . . 13  |-  .+  =  ( +g  `  G )
39 eqid 2443 . . . . . . . . . . . . 13  |-  ( invg `  G )  =  ( invg `  G )
40 tsmsxp.m . . . . . . . . . . . . 13  |-  .-  =  ( -g `  G )
418, 38, 39, 40grpsubval 16072 . . . . . . . . . . . 12  |-  ( ( ( H `  j
)  e.  B  /\  g  e.  B )  ->  ( ( H `  j )  .-  g
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
4237, 41sylan 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .+  ( ( invg `  G ) `  g
) ) )
4342mpteq2dva 4523 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
44 tgpgrp 20555 . . . . . . . . . . . . . 14  |-  ( G  e.  TopGrp  ->  G  e.  Grp )
4513, 44syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  G  e.  Grp )
4645adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  Grp )
478, 39grpinvcl 16074 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  g  e.  B )  ->  ( ( invg `  G ) `  g
)  e.  B )
4846, 47sylan 471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  A )  /\  g  e.  B )  ->  (
( invg `  G ) `  g
)  e.  B )
498, 39grpinvf 16073 . . . . . . . . . . . . 13  |-  ( G  e.  Grp  ->  ( invg `  G ) : B --> B )
5046, 49syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G ) : B --> B )
5150feqmptd 5911 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G )  =  ( g  e.  B  |->  ( ( invg `  G ) `
 g ) ) )
52 eqidd 2444 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  =  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) ) )
53 oveq2 6289 . . . . . . . . . . 11  |-  ( y  =  ( ( invg `  G ) `
 g )  -> 
( ( H `  j )  .+  y
)  =  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) )
5448, 51, 52, 53fmptco 6049 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  =  ( g  e.  B  |->  ( ( H `  j ) 
.+  ( ( invg `  G ) `
 g ) ) ) )
5543, 54eqtr4d 2487 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  =  ( ( y  e.  B  |->  ( ( H `  j
)  .+  y )
)  o.  ( invg `  G ) ) )
5613adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  A )  ->  G  e.  TopGrp )
579, 39grpinvhmeo 20563 . . . . . . . . . . 11  |-  ( G  e.  TopGrp  ->  ( invg `  G )  e.  ( J Homeo J ) )
5856, 57syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  ( invg `  G )  e.  ( J Homeo J ) )
59 eqid 2443 . . . . . . . . . . . 12  |-  ( y  e.  B  |->  ( ( H `  j ) 
.+  y ) )  =  ( y  e.  B  |->  ( ( H `
 j )  .+  y ) )
6059, 8, 38, 9tgplacthmeo 20580 . . . . . . . . . . 11  |-  ( ( G  e.  TopGrp  /\  ( H `  j )  e.  B )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
6156, 37, 60syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  A )  ->  (
y  e.  B  |->  ( ( H `  j
)  .+  y )
)  e.  ( J
Homeo J ) )
62 hmeoco 20251 . . . . . . . . . 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 ) )
6358, 61, 62syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  A )  ->  (
( y  e.  B  |->  ( ( H `  j )  .+  y
) )  o.  ( invg `  G ) )  e.  ( J
Homeo J ) )
6455, 63eqeltrd 2531 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  (
g  e.  B  |->  ( ( H `  j
)  .-  g )
)  e.  ( J
Homeo J ) )
6529adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  L  e.  J )
66 hmeoima 20244 . . . . . . . 8  |-  ( ( ( g  e.  B  |->  ( ( H `  j )  .-  g
) )  e.  ( J Homeo J )  /\  L  e.  J )  ->  ( ( g  e.  B  |->  ( ( H `
 j )  .-  g ) ) " L )  e.  J
)
6764, 65, 66syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( g  e.  B  |->  ( ( H `  j )  .-  g
) ) " L
)  e.  J )
6835, 67eqeltrrd 2532 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ran  ( g  e.  L  |->  ( ( H `  j )  .-  g
) )  e.  J
)
69 tsmsxp.z . . . . . . . . 9  |-  .0.  =  ( 0g `  G )
708, 69, 40grpsubid1 16102 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  ( H `  j )  e.  B )  -> 
( ( H `  j )  .-  .0.  )  =  ( H `  j ) )
7146, 37, 70syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  =  ( H `  j ) )
72 tsmsxp.3 . . . . . . . . 9  |-  ( ph  ->  .0.  e.  L )
7372adantr 465 . . . . . . . 8  |-  ( (
ph  /\  j  e.  A )  ->  .0.  e.  L )
74 ovex 6309 . . . . . . . 8  |-  ( ( H `  j ) 
.-  .0.  )  e.  _V
75 eqid 2443 . . . . . . . . 9  |-  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) )  =  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) )
76 oveq2 6289 . . . . . . . . 9  |-  ( g  =  .0.  ->  (
( H `  j
)  .-  g )  =  ( ( H `
 j )  .-  .0.  ) )
7775, 76elrnmpt1s 5240 . . . . . . . 8  |-  ( (  .0.  e.  L  /\  ( ( H `  j )  .-  .0.  )  e.  _V )  ->  ( ( H `  j )  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `  j ) 
.-  g ) ) )
7873, 74, 77sylancl 662 . . . . . . 7  |-  ( (
ph  /\  j  e.  A )  ->  (
( H `  j
)  .-  .0.  )  e.  ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
7971, 78eqeltrrd 2532 . . . . . 6  |-  ( (
ph  /\  j  e.  A )  ->  ( H `  j )  e.  ran  ( g  e.  L  |->  ( ( H `
 j )  .-  g ) ) )
808, 9, 10, 12, 16, 18, 24, 25, 68, 79tsmsi 20610 . . . . 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 )
) ) )
817, 80syldan 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 )
) ) )
8281ralrimiva 2857 . . 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 ) ) ) )
83 sseq1 3510 . . . . . 6  |-  ( y  =  ( f `  j )  ->  (
y  C_  z  <->  ( f `  j )  C_  z
) )
8483imbi1d 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 ) ) ) ) )
8584ralbidv 2882 . . . 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 ) ) ) ) )
8685ac6sfi 7766 . . 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 )
) ) ) )
874, 82, 86syl2anc 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 ) ) ) ) )
88 frn 5727 . . . . . . . . 9  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  ran  f  C_  ( ~P C  i^i  Fin )
)
8988adantl 466 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ( ~P C  i^i  Fin ) )
90 inss1 3703 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
~P C
9189, 90syl6ss 3501 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  ~P C )
92 sspwuni 4401 . . . . . . 7  |-  ( ran  f  C_  ~P C  <->  U.
ran  f  C_  C
)
9391, 92sylib 196 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  U. ran  f  C_  C )
94 tsmsxp.d . . . . . . . . 9  |-  ( ph  ->  D  e.  ( ~P ( A  X.  C
)  i^i  Fin )
)
95 elfpw 7824 . . . . . . . . . 10  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  <->  ( D  C_  ( A  X.  C
)  /\  D  e.  Fin ) )
9695simplbi 460 . . . . . . . . 9  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  C_  ( A  X.  C
) )
97 rnss 5221 . . . . . . . . 9  |-  ( D 
C_  ( A  X.  C )  ->  ran  D 
C_  ran  ( A  X.  C ) )
9894, 96, 973syl 20 . . . . . . . 8  |-  ( ph  ->  ran  D  C_  ran  ( A  X.  C
) )
99 rnxpss 5429 . . . . . . . 8  |-  ran  ( A  X.  C )  C_  C
10098, 99syl6ss 3501 . . . . . . 7  |-  ( ph  ->  ran  D  C_  C
)
101100adantr 465 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D 
C_  C )
10293, 101unssd 3665 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  C_  C )
1034adantr 465 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  K  e.  Fin )
104 ffn 5721 . . . . . . . . . 10  |-  ( f : K --> ( ~P C  i^i  Fin )  ->  f  Fn  K )
105104adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  f  Fn  K )
106 dffn4 5791 . . . . . . . . 9  |-  ( f  Fn  K  <->  f : K -onto-> ran  f )
107105, 106sylib 196 . . . . . . . 8  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  f : K -onto-> ran  f )
108 fofi 7808 . . . . . . . 8  |-  ( ( K  e.  Fin  /\  f : K -onto-> ran  f
)  ->  ran  f  e. 
Fin )
109103, 107, 108syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  e.  Fin )
110 inss2 3704 . . . . . . . 8  |-  ( ~P C  i^i  Fin )  C_ 
Fin
11189, 110syl6ss 3501 . . . . . . 7  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  f  C_  Fin )
112 unifi 7811 . . . . . . 7  |-  ( ( ran  f  e.  Fin  /\ 
ran  f  C_  Fin )  ->  U. ran  f  e. 
Fin )
113109, 111, 112syl2anc 661 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  U. ran  f  e.  Fin )
11495simprbi 464 . . . . . . . 8  |-  ( D  e.  ( ~P ( A  X.  C )  i^i 
Fin )  ->  D  e.  Fin )
115 rnfi 7807 . . . . . . . 8  |-  ( D  e.  Fin  ->  ran  D  e.  Fin )
11694, 114, 1153syl 20 . . . . . . 7  |-  ( ph  ->  ran  D  e.  Fin )
117116adantr 465 . . . . . 6  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ran  D  e.  Fin )
118 unfi 7789 . . . . . 6  |-  ( ( U. ran  f  e. 
Fin  /\  ran  D  e. 
Fin )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
119113, 117, 118syl2anc 661 . . . . 5  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  Fin )
120 elfpw 7824 . . . . 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 ) )
121102, 119, 120sylanbrc 664 . . . 4  |-  ( (
ph  /\  f : K
--> ( ~P C  i^i  Fin ) )  ->  ( U. ran  f  u.  ran  D )  e.  ( ~P C  i^i  Fin )
)
122121adantrr 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 )
)
123 ssun2 3653 . . . 4  |-  ran  D  C_  ( U. ran  f  u.  ran  D )
124123a1i 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 ) )
125121adantlr 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 ) )
126 fvssunirn 5879 . . . . . . . . . . . . . 14  |-  ( f `
 j )  C_  U.
ran  f
127 ssun1 3652 . . . . . . . . . . . . . 14  |-  U. ran  f  C_  ( U. ran  f  u.  ran  D )
128126, 127sstri 3498 . . . . . . . . . . . . 13  |-  ( f `
 j )  C_  ( U. ran  f  u. 
ran  D )
129 id 22 . . . . . . . . . . . . 13  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  z  =  ( U. ran  f  u. 
ran  D ) )
130128, 129syl5sseqr 3538 . . . . . . . . . . . 12  |-  ( z  =  ( U. ran  f  u.  ran  D )  ->  ( f `  j )  C_  z
)
131 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 ) ) ) )
132130, 131syl 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 ) ) ) )
133 reseq2 5258 . . . . . . . . . . . . 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 ) ) )
134133oveq2d 6297 . . . . . . . . . . . 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 ) ) ) )
135134eleq1d 2512 . . . . . . . . . . 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 ) ) ) )
136132, 135bitrd 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 )
) ) )
137136rspcv 3192 . . . . . . . . 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 ) ) ) )
138125, 137syl 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 )
) ) )
13911ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  G  e. CMnd )
140 cmnmnd 16792 . . . . . . . . . . . . 13  |-  ( G  e. CMnd  ->  G  e.  Mnd )
141139, 140syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  G  e.  Mnd )
142 simplr 755 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  K )
143119adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  e. 
Fin )
144102adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( U. ran  f  u.  ran  D )  C_  C )
145144sselda 3489 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  ( U. ran  f  u. 
ran  D ) )  ->  k  e.  C
)
14619adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  K )  ->  F : ( A  X.  C ) --> B )
147146, 7jca 532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  K )  ->  ( F : ( A  X.  C ) --> B  /\  j  e.  A )
)
148203expa 1197 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F : ( A  X.  C ) --> B  /\  j  e.  A )  /\  k  e.  C )  ->  (
j F k )  e.  B )
149147, 148sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  K )  /\  k  e.  C )  ->  (
j F k )  e.  B )
150149adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  k  e.  C )  ->  (
j F k )  e.  B )
151145, 150syldan 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
)
152 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 ) )
153151, 152fmptd 6040 . . . . . . . . . . . . 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 )
154 ovex 6309 . . . . . . . . . . . . . . 15  |-  ( j F k )  e. 
_V
155154a1i 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 )
156 fvex 5866 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  G )  e. 
_V
15769, 156eqeltri 2527 . . . . . . . . . . . . . . 15  |-  .0.  e.  _V
158157a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  .0.  e.  _V )
159152, 143, 155, 158fsuppmptdm 7842 . . . . . . . . . . . . 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.  )
1608, 69, 139, 143, 153, 159gsumcl 16902 . . . . . . . . . . . 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
)
161 elsn 4028 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { j }  <-> 
y  =  j )
162 ovres 6427 . . . . . . . . . . . . . . . . 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 ) )
163161, 162sylanbr 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 ) )
164 oveq1 6288 . . . . . . . . . . . . . . . . 17  |-  ( y  =  j  ->  (
y F k )  =  ( j F k ) )
165164adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  j  /\  k  e.  ( U. ran  f  u.  ran  D ) )  ->  (
y F k )  =  ( j F k ) )
166163, 165eqtrd 2484 . . . . . . . . . . . . . . 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 ) )
167166mpteq2dva 4523 . . . . . . . . . . . . . 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 ) ) )
168167oveq2d 6297 . . . . . . . . . . . . 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 ) ) ) )
1698, 168gsumsn 16960 . . . . . . . . . . . 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 ) ) ) )
170141, 142, 160, 169syl3anc 1229 . . . . . . . . . . 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 ) ) ) )
171 snfi 7598 . . . . . . . . . . . . 13  |-  { j }  e.  Fin
172171a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  e.  Fin )
17319ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  F : ( A  X.  C ) --> B )
1747adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
j  e.  A )
175174snssd 4160 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  { j }  C_  A )
176 xpss12 5098 . . . . . . . . . . . . . 14  |-  ( ( { j }  C_  A  /\  ( U. ran  f  u.  ran  D ) 
C_  C )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  C_  ( A  X.  C ) )
177175, 144, 176syl2anc 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 ) )
178173, 177fssresd 5742 . . . . . . . . . . . 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 )
179 xpfi 7793 . . . . . . . . . . . . . 14  |-  ( ( { j }  e.  Fin  /\  ( U. ran  f  u.  ran  D )  e.  Fin )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  e.  Fin )
180171, 143, 179sylancr 663 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( { j }  X.  ( U. ran  f  u.  ran  D ) )  e.  Fin )
181178, 180, 158fdmfifsupp 7841 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  -> 
( F  |`  ( { j }  X.  ( U. ran  f  u. 
ran  D ) ) ) finSupp  .0.  )
1828, 69, 139, 172, 143, 178, 181gsumxp 16983 . . . . . . . . . . 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 ) ) ) ) ) )
183144resmptd 5315 . . . . . . . . . . . 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 ) ) )
184183oveq2d 6297 . . . . . . . . . . 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 ) ) ) )
185170, 182, 1843eqtr4rd 2495 . . . . . . . . . 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 ) ) ) ) )
186185eleq1d 2512 . . . . . . . . 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 ) ) ) )
187 ovex 6309 . . . . . . . . . . 11  |-  ( ( H `  j ) 
.-  g )  e. 
_V
18875, 187elrnmpti 5243 . . . . . . . . . 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 ) )
189 isabl 16781 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
19045, 11, 189sylanbrc 664 . . . . . . . . . . . . . . 15  |-  ( ph  ->  G  e.  Abel )
191190ad3antrrr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  G  e.  Abel )
1927, 37syldan 470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  K )  ->  ( H `  j )  e.  B )
193192ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  ( H `  j )  e.  B )
19431ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin ) )  ->  L  C_  B )
195194sselda 3489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  B )
1968, 40, 191, 193, 195ablnncan 16810 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  =  g )
197 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  g  e.  L )
198196, 197eqeltrd 2531 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  j  e.  K )  /\  f : K --> ( ~P C  i^i  Fin )
)  /\  g  e.  L )  ->  (
( H `  j
)  .-  ( ( H `  j )  .-  g ) )  e.  L )
199 oveq2 6289 . . . . . . . . . . . . 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 )
) )
200199eleq1d 2512 . . . . . . . . . . . 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
) )
201198, 200syl5ibrcom 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 ) )
202201rexlimdva 2935 . . . . . . . . . 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 ) )
203188, 202syl5bi 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 ) )
204186, 203sylbid 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 ) )
205138, 204syld 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 ) )
206205an32s 804 . . . . . 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 ) )
207206ralimdva 2851 . . . . 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 ) )
208207impr 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 )
209 fveq2 5856 . . . . . . 7  |-  ( j  =  x  ->  ( H `  j )  =  ( H `  x ) )
210 sneq 4024 . . . . . . . . . 10  |-  ( j  =  x  ->  { j }  =  { x } )
211210xpeq1d 5012 . . . . . . . . 9  |-  ( j  =  x  ->  ( { j }  X.  ( U. ran  f  u. 
ran  D ) )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
212211reseq2d 5263 . . . . . . . 8  |-  ( j  =  x  ->  ( F  |`  ( { j }  X.  ( U. ran  f  u.  ran  D ) ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
213212oveq2d 6297 . . . . . . 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 ) ) ) ) )
214209, 213oveq12d 6299 . . . . . 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 ) ) ) ) ) )
215214eleq1d 2512 . . . . 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 ) )
216215cbvralv 3070 . . . 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 )
217208, 216sylib 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 )
218 sseq2 3511 . . . . 5  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( ran  D  C_  n  <->  ran  D  C_  ( U. ran  f  u.  ran  D ) ) )
219 xpeq2 5004 . . . . . . . . . 10  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( { x }  X.  n )  =  ( { x }  X.  ( U. ran  f  u.  ran  D ) ) )
220219reseq2d 5263 . . . . . . . . 9  |-  ( n  =  ( U. ran  f  u.  ran  D )  ->  ( F  |`  ( { x }  X.  n ) )  =  ( F  |`  ( { x }  X.  ( U. ran  f  u. 
ran  D ) ) ) )
221220oveq2d 6297 . . . . . . . 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 ) ) ) ) )
222221oveq2d 6297 . . . . . . 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 ) ) ) ) ) )
223222eleq1d 2512 . . . . . 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 ) )
224223ralbidv 2882 . . . . 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 ) )
225218, 224anbi12d 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 ) ) )
226225rspcev 3196 . . 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 ) )
227122, 124, 217, 226syl12anc 1227 . 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 ) )
22887, 227exlimddv 1713 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 1383   E.wex 1599    e. wcel 1804   A.wral 2793   E.wrex 2794   _Vcvv 3095    u. cun 3459    i^i cin 3460    C_ wss 3461   ~Pcpw 3997   {csn 4014   U.cuni 4234    |-> cmpt 4495    X. cxp 4987   dom cdm 4989   ran crn 4990    |` cres 4991   "cima 4992    o. ccom 4993    Fn wfn 5573   -->wf 5574   -onto->wfo 5576   ` cfv 5578  (class class class)co 6281   Fincfn 7518   Basecbs 14614   +g cplusg 14679   TopOpenctopn 14801   0gc0g 14819    gsumg cgsu 14820   Mndcmnd 15898   Grpcgrp 16032   invgcminusg 16033   -gcsg 16034  CMndccmn 16777   Abelcabl 16778  TopOnctopon 19373   TopSpctps 19375   Homeochmeo 20232   TopGrpctgp 20548   tsums ctsu 20602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6904  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fsupp 7832  df-oi 7938  df-card 8323  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-2 10601  df-n0 10803  df-z 10872  df-uz 11093  df-fz 11684  df-fzo 11807  df-seq 12090  df-hash 12388  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-ress 14621  df-plusg 14692  df-0g 14821  df-gsum 14822  df-topgen 14823  df-mre 14965  df-mrc 14966  df-acs 14968  df-plusf 15850  df-mgm 15851  df-sgrp 15890  df-mnd 15900  df-submnd 15946  df-grp 16036  df-minusg 16037  df-sbg 16038  df-mulg 16039  df-cntz 16334  df-cmn 16779  df-abl 16780  df-fbas 18395  df-fg 18396  df-top 19377  df-bases 19379  df-topon 19380  df-topsp 19381  df-ntr 19499  df-nei 19577  df-cn 19706  df-cnp 19707  df-tx 20041  df-hmeo 20234  df-fil 20325  df-fm 20417  df-flim 20418  df-flf 20419  df-tmd 20549  df-tgp 20550  df-tsms 20603
This theorem is referenced by:  tsmsxp  20635
  Copyright terms: Public domain W3C validator