Metamath Proof Explorer


Theorem tsmsres

Description: Extend an infinite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 18-Sep-2015) (Revised by AV, 25-Jul-2019)

Ref Expression
Hypotheses tsmsres.b
|- B = ( Base ` G )
tsmsres.z
|- .0. = ( 0g ` G )
tsmsres.1
|- ( ph -> G e. CMnd )
tsmsres.2
|- ( ph -> G e. TopSp )
tsmsres.a
|- ( ph -> A e. V )
tsmsres.f
|- ( ph -> F : A --> B )
tsmsres.s
|- ( ph -> ( F supp .0. ) C_ W )
Assertion tsmsres
|- ( ph -> ( G tsums ( F |` W ) ) = ( G tsums F ) )

Proof

Step Hyp Ref Expression
1 tsmsres.b
 |-  B = ( Base ` G )
2 tsmsres.z
 |-  .0. = ( 0g ` G )
3 tsmsres.1
 |-  ( ph -> G e. CMnd )
4 tsmsres.2
 |-  ( ph -> G e. TopSp )
5 tsmsres.a
 |-  ( ph -> A e. V )
6 tsmsres.f
 |-  ( ph -> F : A --> B )
7 tsmsres.s
 |-  ( ph -> ( F supp .0. ) C_ W )
8 inss1
 |-  ( A i^i W ) C_ A
9 8 sspwi
 |-  ~P ( A i^i W ) C_ ~P A
10 ssrin
 |-  ( ~P ( A i^i W ) C_ ~P A -> ( ~P ( A i^i W ) i^i Fin ) C_ ( ~P A i^i Fin ) )
11 9 10 ax-mp
 |-  ( ~P ( A i^i W ) i^i Fin ) C_ ( ~P A i^i Fin )
12 simpr
 |-  ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> a e. ( ~P ( A i^i W ) i^i Fin ) )
13 11 12 sselid
 |-  ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> a e. ( ~P A i^i Fin ) )
14 elfpw
 |-  ( z e. ( ~P A i^i Fin ) <-> ( z C_ A /\ z e. Fin ) )
15 14 simplbi
 |-  ( z e. ( ~P A i^i Fin ) -> z C_ A )
16 15 adantl
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> z C_ A )
17 16 ssrind
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) C_ ( A i^i W ) )
18 elinel2
 |-  ( z e. ( ~P A i^i Fin ) -> z e. Fin )
19 18 adantl
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin )
20 inss1
 |-  ( z i^i W ) C_ z
21 ssfi
 |-  ( ( z e. Fin /\ ( z i^i W ) C_ z ) -> ( z i^i W ) e. Fin )
22 19 20 21 sylancl
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) e. Fin )
23 elfpw
 |-  ( ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) <-> ( ( z i^i W ) C_ ( A i^i W ) /\ ( z i^i W ) e. Fin ) )
24 17 22 23 sylanbrc
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) )
25 sseq2
 |-  ( b = ( z i^i W ) -> ( a C_ b <-> a C_ ( z i^i W ) ) )
26 ssin
 |-  ( ( a C_ z /\ a C_ W ) <-> a C_ ( z i^i W ) )
27 25 26 bitr4di
 |-  ( b = ( z i^i W ) -> ( a C_ b <-> ( a C_ z /\ a C_ W ) ) )
28 reseq2
 |-  ( b = ( z i^i W ) -> ( ( F |` W ) |` b ) = ( ( F |` W ) |` ( z i^i W ) ) )
29 inss2
 |-  ( z i^i W ) C_ W
30 resabs1
 |-  ( ( z i^i W ) C_ W -> ( ( F |` W ) |` ( z i^i W ) ) = ( F |` ( z i^i W ) ) )
31 29 30 ax-mp
 |-  ( ( F |` W ) |` ( z i^i W ) ) = ( F |` ( z i^i W ) )
32 28 31 eqtrdi
 |-  ( b = ( z i^i W ) -> ( ( F |` W ) |` b ) = ( F |` ( z i^i W ) ) )
33 32 oveq2d
 |-  ( b = ( z i^i W ) -> ( G gsum ( ( F |` W ) |` b ) ) = ( G gsum ( F |` ( z i^i W ) ) ) )
34 33 eleq1d
 |-  ( b = ( z i^i W ) -> ( ( G gsum ( ( F |` W ) |` b ) ) e. u <-> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) )
35 27 34 imbi12d
 |-  ( b = ( z i^i W ) -> ( ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) <-> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) )
36 35 rspcv
 |-  ( ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) )
37 24 36 syl
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) )
38 elfpw
 |-  ( a e. ( ~P ( A i^i W ) i^i Fin ) <-> ( a C_ ( A i^i W ) /\ a e. Fin ) )
39 38 simplbi
 |-  ( a e. ( ~P ( A i^i W ) i^i Fin ) -> a C_ ( A i^i W ) )
40 39 ad2antlr
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> a C_ ( A i^i W ) )
41 inss2
 |-  ( A i^i W ) C_ W
42 40 41 sstrdi
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> a C_ W )
43 42 biantrud
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( a C_ z <-> ( a C_ z /\ a C_ W ) ) )
44 3 ad2antrr
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd )
45 6 ad2antrr
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F : A --> B )
46 45 16 fssresd
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B )
47 6 5 fexd
 |-  ( ph -> F e. _V )
48 47 ad2antrr
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F e. _V )
49 2 fvexi
 |-  .0. e. _V
50 ressuppss
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` z ) supp .0. ) C_ ( F supp .0. ) )
51 48 49 50 sylancl
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F |` z ) supp .0. ) C_ ( F supp .0. ) )
52 7 ad2antrr
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ W )
53 51 52 sstrd
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F |` z ) supp .0. ) C_ W )
54 49 a1i
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> .0. e. _V )
55 46 19 54 fdmfifsupp
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp .0. )
56 1 2 44 19 46 53 55 gsumres
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( ( F |` z ) |` W ) ) = ( G gsum ( F |` z ) ) )
57 resres
 |-  ( ( F |` z ) |` W ) = ( F |` ( z i^i W ) )
58 57 oveq2i
 |-  ( G gsum ( ( F |` z ) |` W ) ) = ( G gsum ( F |` ( z i^i W ) ) )
59 56 58 eqtr3di
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( z i^i W ) ) ) )
60 59 eleq1d
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) )
61 43 60 imbi12d
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) )
62 37 61 sylibrd
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
63 62 ralrimdva
 |-  ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> A. z e. ( ~P A i^i Fin ) ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
64 sseq1
 |-  ( y = a -> ( y C_ z <-> a C_ z ) )
65 64 rspceaimv
 |-  ( ( a e. ( ~P A i^i Fin ) /\ A. z e. ( ~P A i^i Fin ) ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) )
66 13 63 65 syl6an
 |-  ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
67 66 rexlimdva
 |-  ( ph -> ( E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
68 elfpw
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
69 68 simplbi
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
70 69 adantl
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
71 70 ssrind
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) C_ ( A i^i W ) )
72 elinel2
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
73 72 adantl
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
74 inss1
 |-  ( y i^i W ) C_ y
75 ssfi
 |-  ( ( y e. Fin /\ ( y i^i W ) C_ y ) -> ( y i^i W ) e. Fin )
76 73 74 75 sylancl
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. Fin )
77 elfpw
 |-  ( ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) <-> ( ( y i^i W ) C_ ( A i^i W ) /\ ( y i^i W ) e. Fin ) )
78 71 76 77 sylanbrc
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) )
79 69 ad2antlr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> y C_ A )
80 elfpw
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) <-> ( b C_ ( A i^i W ) /\ b e. Fin ) )
81 80 simplbi
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b C_ ( A i^i W ) )
82 81 adantl
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ ( A i^i W ) )
83 82 8 sstrdi
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ A )
84 79 83 unssd
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) C_ A )
85 elinel2
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b e. Fin )
86 unfi
 |-  ( ( y e. Fin /\ b e. Fin ) -> ( y u. b ) e. Fin )
87 73 85 86 syl2an
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) e. Fin )
88 elfpw
 |-  ( ( y u. b ) e. ( ~P A i^i Fin ) <-> ( ( y u. b ) C_ A /\ ( y u. b ) e. Fin ) )
89 84 87 88 sylanbrc
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) e. ( ~P A i^i Fin ) )
90 ssun1
 |-  y C_ ( y u. b )
91 id
 |-  ( z = ( y u. b ) -> z = ( y u. b ) )
92 90 91 sseqtrrid
 |-  ( z = ( y u. b ) -> y C_ z )
93 pm5.5
 |-  ( y C_ z -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
94 92 93 syl
 |-  ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
95 reseq2
 |-  ( z = ( y u. b ) -> ( F |` z ) = ( F |` ( y u. b ) ) )
96 95 oveq2d
 |-  ( z = ( y u. b ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( y u. b ) ) ) )
97 96 eleq1d
 |-  ( z = ( y u. b ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
98 94 97 bitrd
 |-  ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
99 98 rspcv
 |-  ( ( y u. b ) e. ( ~P A i^i Fin ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
100 89 99 syl
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
101 3 ad2antrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> G e. CMnd )
102 87 adantrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y u. b ) e. Fin )
103 6 ad2antrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> F : A --> B )
104 84 adantrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y u. b ) C_ A )
105 103 104 fssresd
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( y u. b ) ) : ( y u. b ) --> B )
106 47 49 jctir
 |-  ( ph -> ( F e. _V /\ .0. e. _V ) )
107 106 ad2antrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F e. _V /\ .0. e. _V ) )
108 ressuppss
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ ( F supp .0. ) )
109 107 108 syl
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ ( F supp .0. ) )
110 7 ad2antrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F supp .0. ) C_ W )
111 109 110 sstrd
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ W )
112 49 a1i
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> .0. e. _V )
113 105 102 112 fdmfifsupp
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( y u. b ) ) finSupp .0. )
114 1 2 101 102 105 111 113 gsumres
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( ( F |` ( y u. b ) ) |` W ) ) = ( G gsum ( F |` ( y u. b ) ) ) )
115 resres
 |-  ( ( F |` ( y u. b ) ) |` W ) = ( F |` ( ( y u. b ) i^i W ) )
116 indir
 |-  ( ( y u. b ) i^i W ) = ( ( y i^i W ) u. ( b i^i W ) )
117 82 41 sstrdi
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ W )
118 117 adantrr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> b C_ W )
119 df-ss
 |-  ( b C_ W <-> ( b i^i W ) = b )
120 118 119 sylib
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( b i^i W ) = b )
121 120 uneq2d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. ( b i^i W ) ) = ( ( y i^i W ) u. b ) )
122 simprr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y i^i W ) C_ b )
123 ssequn1
 |-  ( ( y i^i W ) C_ b <-> ( ( y i^i W ) u. b ) = b )
124 122 123 sylib
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. b ) = b )
125 121 124 eqtrd
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. ( b i^i W ) ) = b )
126 116 125 eqtrid
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y u. b ) i^i W ) = b )
127 126 reseq2d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( ( y u. b ) i^i W ) ) = ( F |` b ) )
128 115 127 eqtrid
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) |` W ) = ( F |` b ) )
129 118 resabs1d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` W ) |` b ) = ( F |` b ) )
130 128 129 eqtr4d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) |` W ) = ( ( F |` W ) |` b ) )
131 130 oveq2d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( ( F |` ( y u. b ) ) |` W ) ) = ( G gsum ( ( F |` W ) |` b ) ) )
132 114 131 eqtr3d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( F |` ( y u. b ) ) ) = ( G gsum ( ( F |` W ) |` b ) ) )
133 132 eleq1d
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u <-> ( G gsum ( ( F |` W ) |` b ) ) e. u ) )
134 133 biimpd
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) )
135 134 expr
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( ( y i^i W ) C_ b -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
136 135 com23
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
137 100 136 syld
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
138 137 ralrimdva
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> A. b e. ( ~P ( A i^i W ) i^i Fin ) ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
139 sseq1
 |-  ( a = ( y i^i W ) -> ( a C_ b <-> ( y i^i W ) C_ b ) )
140 139 rspceaimv
 |-  ( ( ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) /\ A. b e. ( ~P ( A i^i W ) i^i Fin ) ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) )
141 78 138 140 syl6an
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
142 141 rexlimdva
 |-  ( ph -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) )
143 67 142 impbid
 |-  ( ph -> ( E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) <-> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
144 143 imbi2d
 |-  ( ph -> ( ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) <-> ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) )
145 144 ralbidv
 |-  ( ph -> ( A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) <-> A. u e. ( TopOpen ` G ) ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) )
146 145 anbi2d
 |-  ( ph -> ( ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) ) )
147 eqid
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
148 eqid
 |-  ( ~P ( A i^i W ) i^i Fin ) = ( ~P ( A i^i W ) i^i Fin )
149 inex1g
 |-  ( A e. V -> ( A i^i W ) e. _V )
150 5 149 syl
 |-  ( ph -> ( A i^i W ) e. _V )
151 fssres
 |-  ( ( F : A --> B /\ ( A i^i W ) C_ A ) -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
152 6 8 151 sylancl
 |-  ( ph -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
153 resres
 |-  ( ( F |` A ) |` W ) = ( F |` ( A i^i W ) )
154 ffn
 |-  ( F : A --> B -> F Fn A )
155 fnresdm
 |-  ( F Fn A -> ( F |` A ) = F )
156 6 154 155 3syl
 |-  ( ph -> ( F |` A ) = F )
157 156 reseq1d
 |-  ( ph -> ( ( F |` A ) |` W ) = ( F |` W ) )
158 153 157 eqtr3id
 |-  ( ph -> ( F |` ( A i^i W ) ) = ( F |` W ) )
159 158 feq1d
 |-  ( ph -> ( ( F |` ( A i^i W ) ) : ( A i^i W ) --> B <-> ( F |` W ) : ( A i^i W ) --> B ) )
160 152 159 mpbid
 |-  ( ph -> ( F |` W ) : ( A i^i W ) --> B )
161 1 147 148 3 4 150 160 eltsms
 |-  ( ph -> ( x e. ( G tsums ( F |` W ) ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) ) )
162 eqid
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
163 1 147 162 3 4 5 6 eltsms
 |-  ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) ) )
164 146 161 163 3bitr4d
 |-  ( ph -> ( x e. ( G tsums ( F |` W ) ) <-> x e. ( G tsums F ) ) )
165 164 eqrdv
 |-  ( ph -> ( G tsums ( F |` W ) ) = ( G tsums F ) )