Metamath Proof Explorer

Theorem tsmsxplem1

Description: Lemma for tsmsxp . (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b 
|- B = ( Base ` G )
tsmsxp.g 
|- ( ph -> G e. CMnd )
tsmsxp.2 
|- ( ph -> G e. TopGrp )
tsmsxp.a 
|- ( ph -> A e. V )
tsmsxp.c 
|- ( ph -> C e. W )
tsmsxp.f 
|- ( ph -> F : ( A X. C ) --> B )
tsmsxp.h 
|- ( ph -> H : A --> B )
tsmsxp.1 
|- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
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 tsmsxplem1 
|- ( ph -> E. n e. ( ~P C i^i Fin ) ( ran D C_ n /\ A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) e. L ) )

Proof

Step Hyp Ref Expression
1 tsmsxp.b 
 |-  B = ( Base ` G )
2 tsmsxp.g 
 |-  ( ph -> G e. CMnd )
3 tsmsxp.2 
 |-  ( ph -> G e. TopGrp )
4 tsmsxp.a 
 |-  ( ph -> A e. V )
5 tsmsxp.c 
 |-  ( ph -> C e. W )
6 tsmsxp.f 
 |-  ( ph -> F : ( A X. C ) --> B )
7 tsmsxp.h 
 |-  ( ph -> H : A --> B )
8 tsmsxp.1 
 |-  ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
9 tsmsxp.j 
 |-  J = ( TopOpen ` G )
10 tsmsxp.z 
 |-  .0. = ( 0g ` G )
11 tsmsxp.p 
 |-  .+ = ( +g ` G )
12 tsmsxp.m 
 |-  .- = ( -g ` G )
13 tsmsxp.l 
 |-  ( ph -> L e. J )
14 tsmsxp.3 
 |-  ( ph -> .0. e. L )
15 tsmsxp.k 
 |-  ( ph -> K e. ( ~P A i^i Fin ) )
16 tsmsxp.ks 
 |-  ( ph -> dom D C_ K )
17 tsmsxp.d 
 |-  ( ph -> D e. ( ~P ( A X. C ) i^i Fin ) )
18 15 elin2d 
 |-  ( ph -> K e. Fin )
19 elfpw 
 |-  ( K e. ( ~P A i^i Fin ) <-> ( K C_ A /\ K e. Fin ) )
20 19 simplbi 
 |-  ( K e. ( ~P A i^i Fin ) -> K C_ A )
21 15 20 syl 
 |-  ( ph -> K C_ A )
22 21 sselda 
 |-  ( ( ph /\ j e. K ) -> j e. A )
23 eqid 
 |-  ( ~P C i^i Fin ) = ( ~P C i^i Fin )
24 2 adantr 
 |-  ( ( ph /\ j e. A ) -> G e. CMnd )
25 tgptps 
 |-  ( G e. TopGrp -> G e. TopSp )
26 3 25 syl 
 |-  ( ph -> G e. TopSp )
27 26 adantr 
 |-  ( ( ph /\ j e. A ) -> G e. TopSp )
28 5 adantr 
 |-  ( ( ph /\ j e. A ) -> C e. W )
29 fovrn 
 |-  ( ( F : ( A X. C ) --> B /\ j e. A /\ k e. C ) -> ( j F k ) e. B )
30 6 29 syl3an1 
 |-  ( ( ph /\ j e. A /\ k e. C ) -> ( j F k ) e. B )
31 30 3expa 
 |-  ( ( ( ph /\ j e. A ) /\ k e. C ) -> ( j F k ) e. B )
32 31 fmpttd 
 |-  ( ( ph /\ j e. A ) -> ( k e. C |-> ( j F k ) ) : C --> B )
33 df-ima 
 |-  ( ( g e. B |-> ( ( H ` j ) .- g ) ) " L ) = ran ( ( g e. B |-> ( ( H ` j ) .- g ) ) |` L )
34 9 1 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` B ) )
35 3 34 syl 
 |-  ( ph -> J e. ( TopOn ` B ) )
36 toponss 
 |-  ( ( J e. ( TopOn ` B ) /\ L e. J ) -> L C_ B )
37 35 13 36 syl2anc 
 |-  ( ph -> L C_ B )
38 37 adantr 
 |-  ( ( ph /\ j e. A ) -> L C_ B )
39 38 resmptd 
 |-  ( ( ph /\ j e. A ) -> ( ( g e. B |-> ( ( H ` j ) .- g ) ) |` L ) = ( g e. L |-> ( ( H ` j ) .- g ) ) )
40 39 rneqd 
 |-  ( ( ph /\ j e. A ) -> ran ( ( g e. B |-> ( ( H ` j ) .- g ) ) |` L ) = ran ( g e. L |-> ( ( H ` j ) .- g ) ) )
41 33 40 eqtrid 
 |-  ( ( ph /\ j e. A ) -> ( ( g e. B |-> ( ( H ` j ) .- g ) ) " L ) = ran ( g e. L |-> ( ( H ` j ) .- g ) ) )
42 7 ffvelrnda 
 |-  ( ( ph /\ j e. A ) -> ( H ` j ) e. B )
43 eqid 
 |-  ( invg ` G ) = ( invg ` G )
44 1 11 43 12 grpsubval 
 |-  ( ( ( H ` j ) e. B /\ g e. B ) -> ( ( H ` j ) .- g ) = ( ( H ` j ) .+ ( ( invg ` G ) ` g ) ) )
45 42 44 sylan 
 |-  ( ( ( ph /\ j e. A ) /\ g e. B ) -> ( ( H ` j ) .- g ) = ( ( H ` j ) .+ ( ( invg ` G ) ` g ) ) )
46 45 mpteq2dva 
 |-  ( ( ph /\ j e. A ) -> ( g e. B |-> ( ( H ` j ) .- g ) ) = ( g e. B |-> ( ( H ` j ) .+ ( ( invg ` G ) ` g ) ) ) )
47 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
48 3 47 syl 
 |-  ( ph -> G e. Grp )
49 48 adantr 
 |-  ( ( ph /\ j e. A ) -> G e. Grp )
50 1 43 grpinvcl 
 |-  ( ( G e. Grp /\ g e. B ) -> ( ( invg ` G ) ` g ) e. B )
51 49 50 sylan 
 |-  ( ( ( ph /\ j e. A ) /\ g e. B ) -> ( ( invg ` G ) ` g ) e. B )
52 1 43 grpinvf 
 |-  ( G e. Grp -> ( invg ` G ) : B --> B )
53 49 52 syl 
 |-  ( ( ph /\ j e. A ) -> ( invg ` G ) : B --> B )
54 53 feqmptd 
 |-  ( ( ph /\ j e. A ) -> ( invg ` G ) = ( g e. B |-> ( ( invg ` G ) ` g ) ) )
55 eqidd 
 |-  ( ( ph /\ j e. A ) -> ( y e. B |-> ( ( H ` j ) .+ y ) ) = ( y e. B |-> ( ( H ` j ) .+ y ) ) )
56 oveq2 
 |-  ( y = ( ( invg ` G ) ` g ) -> ( ( H ` j ) .+ y ) = ( ( H ` j ) .+ ( ( invg ` G ) ` g ) ) )
57 51 54 55 56 fmptco 
 |-  ( ( ph /\ j e. A ) -> ( ( y e. B |-> ( ( H ` j ) .+ y ) ) o. ( invg ` G ) ) = ( g e. B |-> ( ( H ` j ) .+ ( ( invg ` G ) ` g ) ) ) )
58 46 57 eqtr4d 
 |-  ( ( ph /\ j e. A ) -> ( g e. B |-> ( ( H ` j ) .- g ) ) = ( ( y e. B |-> ( ( H ` j ) .+ y ) ) o. ( invg ` G ) ) )
59 3 adantr 
 |-  ( ( ph /\ j e. A ) -> G e. TopGrp )
60 9 43 grpinvhmeo 
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( J Homeo J ) )
61 59 60 syl 
 |-  ( ( ph /\ j e. A ) -> ( invg ` G ) e. ( J Homeo J ) )
62 eqid 
 |-  ( y e. B |-> ( ( H ` j ) .+ y ) ) = ( y e. B |-> ( ( H ` j ) .+ y ) )
63 62 1 11 9 tgplacthmeo 
 |-  ( ( G e. TopGrp /\ ( H ` j ) e. B ) -> ( y e. B |-> ( ( H ` j ) .+ y ) ) e. ( J Homeo J ) )
64 59 42 63 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( y e. B |-> ( ( H ` j ) .+ y ) ) e. ( J Homeo J ) )
65 hmeoco 
 |-  ( ( ( 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 ) )
66 61 64 65 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( ( y e. B |-> ( ( H ` j ) .+ y ) ) o. ( invg ` G ) ) e. ( J Homeo J ) )
67 58 66 eqeltrd 
 |-  ( ( ph /\ j e. A ) -> ( g e. B |-> ( ( H ` j ) .- g ) ) e. ( J Homeo J ) )
68 13 adantr 
 |-  ( ( ph /\ j e. A ) -> L e. J )
69 hmeoima 
 |-  ( ( ( g e. B |-> ( ( H ` j ) .- g ) ) e. ( J Homeo J ) /\ L e. J ) -> ( ( g e. B |-> ( ( H ` j ) .- g ) ) " L ) e. J )
70 67 68 69 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( ( g e. B |-> ( ( H ` j ) .- g ) ) " L ) e. J )
71 41 70 eqeltrrd 
 |-  ( ( ph /\ j e. A ) -> ran ( g e. L |-> ( ( H ` j ) .- g ) ) e. J )
72 1 10 12 grpsubid1 
 |-  ( ( G e. Grp /\ ( H ` j ) e. B ) -> ( ( H ` j ) .- .0. ) = ( H ` j ) )
73 49 42 72 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( ( H ` j ) .- .0. ) = ( H ` j ) )
74 14 adantr 
 |-  ( ( ph /\ j e. A ) -> .0. e. L )
75 ovex 
 |-  ( ( H ` j ) .- .0. ) e. _V
76 eqid 
 |-  ( g e. L |-> ( ( H ` j ) .- g ) ) = ( g e. L |-> ( ( H ` j ) .- g ) )
77 oveq2 
 |-  ( g = .0. -> ( ( H ` j ) .- g ) = ( ( H ` j ) .- .0. ) )
78 76 77 elrnmpt1s 
 |-  ( ( .0. e. L /\ ( ( H ` j ) .- .0. ) e. _V ) -> ( ( H ` j ) .- .0. ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) )
79 74 75 78 sylancl 
 |-  ( ( ph /\ j e. A ) -> ( ( H ` j ) .- .0. ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) )
80 73 79 eqeltrrd 
 |-  ( ( ph /\ j e. A ) -> ( H ` j ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) )
81 1 9 23 24 27 28 32 8 71 80 tsmsi 
 |-  ( ( ph /\ j e. A ) -> E. y e. ( ~P C i^i Fin ) A. z e. ( ~P C i^i Fin ) ( y C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
82 22 81 syldan 
 |-  ( ( ph /\ j e. K ) -> E. y e. ( ~P C i^i Fin ) A. z e. ( ~P C i^i Fin ) ( y C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
83 82 ralrimiva 
 |-  ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
84 sseq1 
 |-  ( y = ( f ` j ) -> ( y C_ z <-> ( f ` j ) C_ z ) )
85 84 imbi1d 
 |-  ( y = ( f ` j ) -> ( ( y C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) <-> ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) )
86 85 ralbidv 
 |-  ( y = ( f ` j ) -> ( A. z e. ( ~P C i^i Fin ) ( y C_ z -> ( G gsum ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) )
87 86 ac6sfi 
 |-  ( ( 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 gsum ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) )
88 18 83 87 syl2anc 
 |-  ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) )
89 frn 
 |-  ( f : K --> ( ~P C i^i Fin ) -> ran f C_ ( ~P C i^i Fin ) )
90 89 adantl 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran f C_ ( ~P C i^i Fin ) )
91 inss1 
 |-  ( ~P C i^i Fin ) C_ ~P C
92 90 91 sstrdi 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran f C_ ~P C )
93 sspwuni 
 |-  ( ran f C_ ~P C <-> U. ran f C_ C )
94 92 93 sylib 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> U. ran f C_ C )
95 elfpw 
 |-  ( D e. ( ~P ( A X. C ) i^i Fin ) <-> ( D C_ ( A X. C ) /\ D e. Fin ) )
96 95 simplbi 
 |-  ( D e. ( ~P ( A X. C ) i^i Fin ) -> D C_ ( A X. C ) )
97 rnss 
 |-  ( D C_ ( A X. C ) -> ran D C_ ran ( A X. C ) )
98 17 96 97 3syl 
 |-  ( ph -> ran D C_ ran ( A X. C ) )
99 rnxpss 
 |-  ran ( A X. C ) C_ C
100 98 99 sstrdi 
 |-  ( ph -> ran D C_ C )
101 100 adantr 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran D C_ C )
102 94 101 unssd 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ( U. ran f u. ran D ) C_ C )
103 18 adantr 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> K e. Fin )
104 ffn 
 |-  ( f : K --> ( ~P C i^i Fin ) -> f Fn K )
105 104 adantl 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> f Fn K )
106 dffn4 
 |-  ( f Fn K <-> f : K -onto-> ran f )
107 105 106 sylib 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> f : K -onto-> ran f )
108 fofi 
 |-  ( ( K e. Fin /\ f : K -onto-> ran f ) -> ran f e. Fin )
109 103 107 108 syl2anc 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran f e. Fin )
110 inss2 
 |-  ( ~P C i^i Fin ) C_ Fin
111 90 110 sstrdi 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran f C_ Fin )
112 unifi 
 |-  ( ( ran f e. Fin /\ ran f C_ Fin ) -> U. ran f e. Fin )
113 109 111 112 syl2anc 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> U. ran f e. Fin )
114 elinel2 
 |-  ( D e. ( ~P ( A X. C ) i^i Fin ) -> D e. Fin )
115 rnfi 
 |-  ( D e. Fin -> ran D e. Fin )
116 17 114 115 3syl 
 |-  ( ph -> ran D e. Fin )
117 116 adantr 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ran D e. Fin )
118 unfi 
 |-  ( ( U. ran f e. Fin /\ ran D e. Fin ) -> ( U. ran f u. ran D ) e. Fin )
119 113 117 118 syl2anc 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ( U. ran f u. ran D ) e. Fin )
120 elfpw 
 |-  ( ( 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 ) )
121 102 119 120 sylanbrc 
 |-  ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) -> ( U. ran f u. ran D ) e. ( ~P C i^i Fin ) )
122 121 adantrr 
 |-  ( ( 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 gsum ( ( 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 
 |-  ran D C_ ( U. ran f u. ran D )
124 123 a1i 
 |-  ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) ) -> ran D C_ ( U. ran f u. ran D ) )
125 121 adantlr 
 |-  ( ( ( 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 
 |-  ( f ` j ) C_ U. ran f
127 ssun1 
 |-  U. ran f C_ ( U. ran f u. ran D )
128 126 127 sstri 
 |-  ( f ` j ) C_ ( U. ran f u. ran D )
129 id 
 |-  ( z = ( U. ran f u. ran D ) -> z = ( U. ran f u. ran D ) )
130 128 129 sseqtrrid 
 |-  ( z = ( U. ran f u. ran D ) -> ( f ` j ) C_ z )
131 pm5.5 
 |-  ( ( f ` j ) C_ z -> ( ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) <-> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
132 130 131 syl 
 |-  ( z = ( U. ran f u. ran D ) -> ( ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) <-> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
133 reseq2 
 |-  ( 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 ) ) )
134 133 oveq2d 
 |-  ( z = ( U. ran f u. ran D ) -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) = ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) )
135 134 eleq1d 
 |-  ( z = ( U. ran f u. ran D ) -> ( ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) <-> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
136 132 135 bitrd 
 |-  ( z = ( U. ran f u. ran D ) -> ( ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) <-> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
137 136 rspcv 
 |-  ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
138 125 137 syl 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( A. z e. ( ~P C i^i Fin ) ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
139 2 ad2antrr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> G e. CMnd )
140 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
141 139 140 syl 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> G e. Mnd )
142 simplr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> j e. K )
143 119 adantlr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( U. ran f u. ran D ) e. Fin )
144 102 adantlr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( U. ran f u. ran D ) C_ C )
145 144 sselda 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ k e. ( U. ran f u. ran D ) ) -> k e. C )
146 6 adantr 
 |-  ( ( ph /\ j e. K ) -> F : ( A X. C ) --> B )
147 146 22 jca 
 |-  ( ( ph /\ j e. K ) -> ( F : ( A X. C ) --> B /\ j e. A ) )
148 29 3expa 
 |-  ( ( ( F : ( A X. C ) --> B /\ j e. A ) /\ k e. C ) -> ( j F k ) e. B )
149 147 148 sylan 
 |-  ( ( ( ph /\ j e. K ) /\ k e. C ) -> ( j F k ) e. B )
150 149 adantlr 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ k e. C ) -> ( j F k ) e. B )
151 145 150 syldan 
 |-  ( ( ( ( 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 151 fmpttd 
 |-  ( ( ( 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 )
153 eqid 
 |-  ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) = ( k e. ( U. ran f u. ran D ) |-> ( j F k ) )
154 ovexd 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ k e. ( U. ran f u. ran D ) ) -> ( j F k ) e. _V )
155 10 fvexi 
 |-  .0. e. _V
156 155 a1i 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> .0. e. _V )
157 153 143 154 156 fsuppmptdm 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) finSupp .0. )
158 1 10 139 143 152 157 gsumcl 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) e. B )
159 velsn 
 |-  ( y e. { j } <-> y = j )
160 ovres 
 |-  ( ( 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 ) )
161 159 160 sylanbr 
 |-  ( ( y = j /\ k e. ( U. ran f u. ran D ) ) -> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) = ( y F k ) )
162 oveq1 
 |-  ( y = j -> ( y F k ) = ( j F k ) )
163 162 adantr 
 |-  ( ( y = j /\ k e. ( U. ran f u. ran D ) ) -> ( y F k ) = ( j F k ) )
164 161 163 eqtrd 
 |-  ( ( y = j /\ k e. ( U. ran f u. ran D ) ) -> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) = ( j F k ) )
165 164 mpteq2dva 
 |-  ( 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 ) ) )
166 165 oveq2d 
 |-  ( y = j -> ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) ) ) = ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) )
167 1 166 gsumsn 
 |-  ( ( G e. Mnd /\ j e. K /\ ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) e. B ) -> ( G gsum ( y e. { j } |-> ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) ) ) ) ) = ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) )
168 141 142 158 167 syl3anc 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( G gsum ( y e. { j } |-> ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) ) ) ) ) = ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) )
169 snfi 
 |-  { j } e. Fin
170 169 a1i 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> { j } e. Fin )
171 6 ad2antrr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> F : ( A X. C ) --> B )
172 22 adantr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> j e. A )
173 172 snssd 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> { j } C_ A )
174 xpss12 
 |-  ( ( { j } C_ A /\ ( U. ran f u. ran D ) C_ C ) -> ( { j } X. ( U. ran f u. ran D ) ) C_ ( A X. C ) )
175 173 144 174 syl2anc 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( { j } X. ( U. ran f u. ran D ) ) C_ ( A X. C ) )
176 171 175 fssresd 
 |-  ( ( ( 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 )
177 xpfi 
 |-  ( ( { j } e. Fin /\ ( U. ran f u. ran D ) e. Fin ) -> ( { j } X. ( U. ran f u. ran D ) ) e. Fin )
178 169 143 177 sylancr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( { j } X. ( U. ran f u. ran D ) ) e. Fin )
179 176 178 156 fdmfifsupp 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) finSupp .0. )
180 1 10 139 170 143 176 179 gsumxp 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( G gsum ( y e. { j } |-> ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( y ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) k ) ) ) ) ) )
181 144 resmptd 
 |-  ( ( ( 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 ) ) )
182 181 oveq2d 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) = ( G gsum ( k e. ( U. ran f u. ran D ) |-> ( j F k ) ) ) )
183 168 180 182 3eqtr4rd 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) = ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) )
184 183 eleq1d 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) <-> ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) )
185 ovex 
 |-  ( ( H ` j ) .- g ) e. _V
186 76 185 elrnmpti 
 |-  ( ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) <-> E. g e. L ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( ( H ` j ) .- g ) )
187 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
188 48 2 187 sylanbrc 
 |-  ( ph -> G e. Abel )
189 188 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> G e. Abel )
190 22 42 syldan 
 |-  ( ( ph /\ j e. K ) -> ( H ` j ) e. B )
191 190 ad2antrr 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> ( H ` j ) e. B )
192 37 ad2antrr 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> L C_ B )
193 192 sselda 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> g e. B )
194 1 12 189 191 193 ablnncan 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> ( ( H ` j ) .- ( ( H ` j ) .- g ) ) = g )
195 simpr 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> g e. L )
196 194 195 eqeltrd 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> ( ( H ` j ) .- ( ( H ` j ) .- g ) ) e. L )
197 oveq2 
 |-  ( ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( ( H ` j ) .- g ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) = ( ( H ` j ) .- ( ( H ` j ) .- g ) ) )
198 197 eleq1d 
 |-  ( ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( ( H ` j ) .- g ) -> ( ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L <-> ( ( H ` j ) .- ( ( H ` j ) .- g ) ) e. L ) )
199 196 198 syl5ibrcom 
 |-  ( ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) /\ g e. L ) -> ( ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( ( H ` j ) .- g ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
200 199 rexlimdva 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( E. g e. L ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( ( H ` j ) .- g ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
201 186 200 syl5bi 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
202 184 201 sylbid 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( ( G gsum ( ( k e. C |-> ( j F k ) ) |` ( U. ran f u. ran D ) ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
203 138 202 syld 
 |-  ( ( ( ph /\ j e. K ) /\ f : K --> ( ~P C i^i Fin ) ) -> ( A. z e. ( ~P C i^i Fin ) ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
204 203 an32s 
 |-  ( ( ( ph /\ f : K --> ( ~P C i^i Fin ) ) /\ j e. K ) -> ( A. z e. ( ~P C i^i Fin ) ( ( f ` j ) C_ z -> ( G gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
205 204 ralimdva 
 |-  ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) -> A. j e. K ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
206 205 impr 
 |-  ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) ) -> A. j e. K ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L )
207 fveq2 
 |-  ( j = x -> ( H ` j ) = ( H ` x ) )
208 sneq 
 |-  ( j = x -> { j } = { x } )
209 208 xpeq1d 
 |-  ( j = x -> ( { j } X. ( U. ran f u. ran D ) ) = ( { x } X. ( U. ran f u. ran D ) ) )
210 209 reseq2d 
 |-  ( j = x -> ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) = ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) )
211 210 oveq2d 
 |-  ( j = x -> ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) = ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) )
212 207 211 oveq12d 
 |-  ( j = x -> ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) = ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) )
213 212 eleq1d 
 |-  ( j = x -> ( ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L <-> ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
214 213 cbvralvw 
 |-  ( A. j e. K ( ( H ` j ) .- ( G gsum ( F |` ( { j } X. ( U. ran f u. ran D ) ) ) ) ) e. L <-> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L )
215 206 214 sylib 
 |-  ( ( 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 gsum ( ( k e. C |-> ( j F k ) ) |` z ) ) e. ran ( g e. L |-> ( ( H ` j ) .- g ) ) ) ) ) -> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L )
216 sseq2 
 |-  ( n = ( U. ran f u. ran D ) -> ( ran D C_ n <-> ran D C_ ( U. ran f u. ran D ) ) )
217 xpeq2 
 |-  ( n = ( U. ran f u. ran D ) -> ( { x } X. n ) = ( { x } X. ( U. ran f u. ran D ) ) )
218 217 reseq2d 
 |-  ( n = ( U. ran f u. ran D ) -> ( F |` ( { x } X. n ) ) = ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) )
219 218 oveq2d 
 |-  ( n = ( U. ran f u. ran D ) -> ( G gsum ( F |` ( { x } X. n ) ) ) = ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) )
220 219 oveq2d 
 |-  ( n = ( U. ran f u. ran D ) -> ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) = ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) )
221 220 eleq1d 
 |-  ( n = ( U. ran f u. ran D ) -> ( ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) e. L <-> ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
222 221 ralbidv 
 |-  ( n = ( U. ran f u. ran D ) -> ( A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) e. L <-> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) )
223 216 222 anbi12d 
 |-  ( n = ( U. ran f u. ran D ) -> ( ( ran D C_ n /\ A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) e. L ) <-> ( ran D C_ ( U. ran f u. ran D ) /\ A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. ( U. ran f u. ran D ) ) ) ) ) e. L ) ) )
224 223 rspcev 
 |-  ( ( ( 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 gsum ( 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 gsum ( F |` ( { x } X. n ) ) ) ) e. L ) )
225 122 124 215 224 syl12anc 
 |-  ( ( 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 gsum ( ( 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 gsum ( F |` ( { x } X. n ) ) ) ) e. L ) )
226 88 225 exlimddv 
 |-  ( ph -> E. n e. ( ~P C i^i Fin ) ( ran D C_ n /\ A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. n ) ) ) ) e. L ) )