# 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}={\mathrm{Base}}_{{G}}$
tsmsres.z
tsmsres.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
tsmsres.2 ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
tsmsres.a ${⊢}{\phi }\to {A}\in {V}$
tsmsres.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
tsmsres.s
Assertion tsmsres ${⊢}{\phi }\to {G}\mathrm{tsums}\left({{F}↾}_{{W}}\right)={G}\mathrm{tsums}{F}$

### Proof

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