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 dfss2 
 |-  ( 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 ) )