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 ˙ = 0 G
tsmsres.1 φ G CMnd
tsmsres.2 φ G TopSp
tsmsres.a φ A V
tsmsres.f φ F : A B
tsmsres.s φ F supp 0 ˙ W
Assertion tsmsres φ G tsums F W = G tsums F

Proof

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