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 sseldi 
 |-  ( ( 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 resres 
 |-  ( ( F |` z ) |` W ) = ( F |` ( z i^i W ) )
45 44 oveq2i 
 |-  ( G gsum ( ( F |` z ) |` W ) ) = ( G gsum ( F |` ( z i^i W ) ) )
46 3 ad2antrr 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd )
47 6 ad2antrr 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F : A --> B )
48 47 16 fssresd 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B )
49 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
50 6 5 49 syl2anc 
 |-  ( ph -> F e. _V )
51 50 ad2antrr 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F e. _V )
52 2 fvexi 
 |-  .0. e. _V
53 ressuppss 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` z ) supp .0. ) C_ ( F supp .0. ) )
54 51 52 53 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. ) )
55 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 )
56 54 55 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 )
57 52 a1i 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> .0. e. _V )
58 48 19 57 fdmfifsupp 
 |-  ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp .0. )
59 1 2 46 19 48 56 58 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 ) ) )
60 45 59 syl5reqr 
 |-  ( ( ( 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 ) ) ) )
61 60 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 ) )
62 43 61 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 ) ) )
63 37 62 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 ) ) )
64 63 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 ) ) )
65 sseq1 
 |-  ( y = a -> ( y C_ z <-> a C_ z ) )
66 65 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 ) )
67 13 64 66 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 ) ) )
68 67 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 ) ) )
69 elfpw 
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
70 69 simplbi 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
71 70 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
72 71 ssrind 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) C_ ( A i^i W ) )
73 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
74 73 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
75 inss1 
 |-  ( y i^i W ) C_ y
76 ssfi 
 |-  ( ( y e. Fin /\ ( y i^i W ) C_ y ) -> ( y i^i W ) e. Fin )
77 74 75 76 sylancl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. Fin )
78 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 ) )
79 72 77 78 sylanbrc 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) )
80 70 ad2antlr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> y C_ A )
81 elfpw 
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) <-> ( b C_ ( A i^i W ) /\ b e. Fin ) )
82 81 simplbi 
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b C_ ( A i^i W ) )
83 82 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 ) )
84 83 8 sstrdi 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ A )
85 80 84 unssd 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) C_ A )
86 elinel2 
 |-  ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b e. Fin )
87 unfi 
 |-  ( ( y e. Fin /\ b e. Fin ) -> ( y u. b ) e. Fin )
88 74 86 87 syl2an 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) e. Fin )
89 elfpw 
 |-  ( ( y u. b ) e. ( ~P A i^i Fin ) <-> ( ( y u. b ) C_ A /\ ( y u. b ) e. Fin ) )
90 85 88 89 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 ) )
91 ssun1 
 |-  y C_ ( y u. b )
92 id 
 |-  ( z = ( y u. b ) -> z = ( y u. b ) )
93 91 92 sseqtrrid 
 |-  ( z = ( y u. b ) -> y C_ z )
94 pm5.5 
 |-  ( y C_ z -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
95 93 94 syl 
 |-  ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
96 reseq2 
 |-  ( z = ( y u. b ) -> ( F |` z ) = ( F |` ( y u. b ) ) )
97 96 oveq2d 
 |-  ( z = ( y u. b ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( y u. b ) ) ) )
98 97 eleq1d 
 |-  ( z = ( y u. b ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
99 95 98 bitrd 
 |-  ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) )
100 99 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 ) )
101 90 100 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 ) )
102 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 )
103 88 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 )
104 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 )
105 85 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 )
106 104 105 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 )
107 50 52 jctir 
 |-  ( ph -> ( F e. _V /\ .0. e. _V ) )
108 107 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 ) )
109 ressuppss 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ ( F supp .0. ) )
110 108 109 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. ) )
111 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 )
112 110 111 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 )
113 52 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 )
114 106 103 113 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. )
115 1 2 102 103 106 112 114 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 ) ) ) )
116 resres 
 |-  ( ( F |` ( y u. b ) ) |` W ) = ( F |` ( ( y u. b ) i^i W ) )
117 indir 
 |-  ( ( y u. b ) i^i W ) = ( ( y i^i W ) u. ( b i^i W ) )
118 83 41 sstrdi 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ W )
119 118 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 )
120 df-ss 
 |-  ( b C_ W <-> ( b i^i W ) = b )
121 119 120 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 )
122 121 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 ) )
123 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 )
124 ssequn1 
 |-  ( ( y i^i W ) C_ b <-> ( ( y i^i W ) u. b ) = b )
125 123 124 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 )
126 122 125 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 )
127 117 126 syl5eq 
 |-  ( ( ( 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 )
128 127 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 ) )
129 116 128 syl5eq 
 |-  ( ( ( 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 ) )
130 119 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 ) )
131 129 130 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 ) )
132 131 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 ) ) )
133 115 132 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 ) ) )
134 133 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 ) )
135 134 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 ) )
136 135 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 ) ) )
137 136 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 ) ) )
138 101 137 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 ) ) )
139 138 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 ) ) )
140 sseq1 
 |-  ( a = ( y i^i W ) -> ( a C_ b <-> ( y i^i W ) C_ b ) )
141 140 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 ) )
142 79 139 141 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 ) ) )
143 142 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 ) ) )
144 68 143 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 ) ) )
145 144 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 ) ) ) )
146 145 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 ) ) ) )
147 146 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 ) ) ) ) )
148 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
149 eqid 
 |-  ( ~P ( A i^i W ) i^i Fin ) = ( ~P ( A i^i W ) i^i Fin )
150 inex1g 
 |-  ( A e. V -> ( A i^i W ) e. _V )
151 5 150 syl 
 |-  ( ph -> ( A i^i W ) e. _V )
152 fssres 
 |-  ( ( F : A --> B /\ ( A i^i W ) C_ A ) -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
153 6 8 152 sylancl 
 |-  ( ph -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B )
154 resres 
 |-  ( ( F |` A ) |` W ) = ( F |` ( A i^i W ) )
155 ffn 
 |-  ( F : A --> B -> F Fn A )
156 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
157 6 155 156 3syl 
 |-  ( ph -> ( F |` A ) = F )
158 157 reseq1d 
 |-  ( ph -> ( ( F |` A ) |` W ) = ( F |` W ) )
159 154 158 eqtr3id 
 |-  ( ph -> ( F |` ( A i^i W ) ) = ( F |` W ) )
160 159 feq1d 
 |-  ( ph -> ( ( F |` ( A i^i W ) ) : ( A i^i W ) --> B <-> ( F |` W ) : ( A i^i W ) --> B ) )
161 153 160 mpbid 
 |-  ( ph -> ( F |` W ) : ( A i^i W ) --> B )
162 1 148 149 3 4 151 161 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 ) ) ) ) )
163 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
164 1 148 163 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 ) ) ) ) )
165 147 162 164 3bitr4d 
 |-  ( ph -> ( x e. ( G tsums ( F |` W ) ) <-> x e. ( G tsums F ) ) )
166 165 eqrdv 
 |-  ( ph -> ( G tsums ( F |` W ) ) = ( G tsums F ) )