Metamath Proof Explorer

Theorem tsmsf1o

Description: Re-index an infinite group sum using a bijection. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tsmsf1o.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
tsmsf1o.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
tsmsf1o.2 ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
tsmsf1o.a ${⊢}{\phi }\to {A}\in {V}$
tsmsf1o.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
tsmsf1o.s ${⊢}{\phi }\to {H}:{C}\underset{1-1 onto}{⟶}{A}$
Assertion tsmsf1o ${⊢}{\phi }\to {G}\mathrm{tsums}{F}={G}\mathrm{tsums}\left({F}\circ {H}\right)$

Proof

Step Hyp Ref Expression
1 tsmsf1o.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 tsmsf1o.1 ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
3 tsmsf1o.2 ${⊢}{\phi }\to {G}\in \mathrm{TopSp}$
4 tsmsf1o.a ${⊢}{\phi }\to {A}\in {V}$
5 tsmsf1o.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
6 tsmsf1o.s ${⊢}{\phi }\to {H}:{C}\underset{1-1 onto}{⟶}{A}$
7 f1opwfi ${⊢}{H}:{C}\underset{1-1 onto}{⟶}{A}\to \left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}𝒫{A}\cap \mathrm{Fin}$
8 6 7 syl ${⊢}{\phi }\to \left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}𝒫{A}\cap \mathrm{Fin}$
9 f1of ${⊢}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}𝒫{A}\cap \mathrm{Fin}\to \left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}⟶𝒫{A}\cap \mathrm{Fin}$
10 8 9 syl ${⊢}{\phi }\to \left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}⟶𝒫{A}\cap \mathrm{Fin}$
11 eqid ${⊢}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)=\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)$
12 11 fmpt ${⊢}\forall {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{a}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)↔\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}⟶𝒫{A}\cap \mathrm{Fin}$
13 10 12 sylibr ${⊢}{\phi }\to \forall {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{a}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
14 sseq1 ${⊢}{y}={H}\left[{a}\right]\to \left({y}\subseteq {z}↔{H}\left[{a}\right]\subseteq {z}\right)$
15 14 imbi1d ${⊢}{y}={H}\left[{a}\right]\to \left(\left({y}\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
16 15 ralbidv ${⊢}{y}={H}\left[{a}\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)↔\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
17 11 16 rexrnmptw ${⊢}\forall {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{a}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to \left(\exists {y}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\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)↔\exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
18 13 17 syl ${⊢}{\phi }\to \left(\exists {y}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\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)↔\exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
19 f1ofo ${⊢}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}𝒫{A}\cap \mathrm{Fin}\to \left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{onto}{⟶}𝒫{A}\cap \mathrm{Fin}$
20 forn ${⊢}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}\underset{onto}{⟶}𝒫{A}\cap \mathrm{Fin}\to \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)=𝒫{A}\cap \mathrm{Fin}$
21 8 19 20 3syl ${⊢}{\phi }\to \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)=𝒫{A}\cap \mathrm{Fin}$
22 21 rexeqdv ${⊢}{\phi }\to \left(\exists {y}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\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)↔\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)$
23 imaeq2 ${⊢}{a}={b}\to {H}\left[{a}\right]={H}\left[{b}\right]$
24 23 cbvmptv ${⊢}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)=\left({b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{b}\right]\right)$
25 24 fmpt ${⊢}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{b}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)↔\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right):𝒫{C}\cap \mathrm{Fin}⟶𝒫{A}\cap \mathrm{Fin}$
26 10 25 sylibr ${⊢}{\phi }\to \forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{b}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
27 sseq2 ${⊢}{z}={H}\left[{b}\right]\to \left({H}\left[{a}\right]\subseteq {z}↔{H}\left[{a}\right]\subseteq {H}\left[{b}\right]\right)$
28 reseq2 ${⊢}{z}={H}\left[{b}\right]\to {{F}↾}_{{z}}={{F}↾}_{{H}\left[{b}\right]}$
29 28 oveq2d ${⊢}{z}={H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)={\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)$
30 29 eleq1d ${⊢}{z}={H}\left[{b}\right]\to \left({\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}↔{\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)$
31 27 30 imbi12d ${⊢}{z}={H}\left[{b}\right]\to \left(\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)\right)$
32 24 31 ralrnmptw ${⊢}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{H}\left[{b}\right]\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to \left(\forall {z}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)\right)$
33 26 32 syl ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)\right)$
34 21 raleqdv ${⊢}{\phi }\to \left(\forall {z}\in \mathrm{ran}\left({a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)⟼{H}\left[{a}\right]\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
35 33 34 bitr3d ${⊢}{\phi }\to \left(\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)↔\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
36 35 adantr ${⊢}\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left(\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)↔\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)\right)$
37 f1of1 ${⊢}{H}:{C}\underset{1-1 onto}{⟶}{A}\to {H}:{C}\underset{1-1}{⟶}{A}$
38 6 37 syl ${⊢}{\phi }\to {H}:{C}\underset{1-1}{⟶}{A}$
39 38 ad2antrr ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {H}:{C}\underset{1-1}{⟶}{A}$
40 elfpw ${⊢}{a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)↔\left({a}\subseteq {C}\wedge {a}\in \mathrm{Fin}\right)$
41 40 simplbi ${⊢}{a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\to {a}\subseteq {C}$
42 41 ad2antlr ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {a}\subseteq {C}$
43 elfpw ${⊢}{b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)↔\left({b}\subseteq {C}\wedge {b}\in \mathrm{Fin}\right)$
44 43 simplbi ${⊢}{b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\to {b}\subseteq {C}$
45 44 adantl ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {b}\subseteq {C}$
46 f1imass ${⊢}\left({H}:{C}\underset{1-1}{⟶}{A}\wedge \left({a}\subseteq {C}\wedge {b}\subseteq {C}\right)\right)\to \left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]↔{a}\subseteq {b}\right)$
47 39 42 45 46 syl12anc ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]↔{a}\subseteq {b}\right)$
48 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
49 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {G}\in \mathrm{CMnd}$
50 elinel2 ${⊢}{b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\to {b}\in \mathrm{Fin}$
51 50 adantl ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {b}\in \mathrm{Fin}$
52 f1ores ${⊢}\left({H}:{C}\underset{1-1}{⟶}{A}\wedge {b}\subseteq {C}\right)\to \left({{H}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{H}\left[{b}\right]$
53 39 45 52 syl2anc ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left({{H}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{H}\left[{b}\right]$
54 f1ofo ${⊢}\left({{H}↾}_{{b}}\right):{b}\underset{1-1 onto}{⟶}{H}\left[{b}\right]\to \left({{H}↾}_{{b}}\right):{b}\underset{onto}{⟶}{H}\left[{b}\right]$
55 53 54 syl ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left({{H}↾}_{{b}}\right):{b}\underset{onto}{⟶}{H}\left[{b}\right]$
56 fofi ${⊢}\left({b}\in \mathrm{Fin}\wedge \left({{H}↾}_{{b}}\right):{b}\underset{onto}{⟶}{H}\left[{b}\right]\right)\to {H}\left[{b}\right]\in \mathrm{Fin}$
57 51 55 56 syl2anc ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {H}\left[{b}\right]\in \mathrm{Fin}$
58 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {F}:{A}⟶{B}$
59 imassrn ${⊢}{H}\left[{b}\right]\subseteq \mathrm{ran}{H}$
60 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {H}:{C}\underset{1-1 onto}{⟶}{A}$
61 f1ofo ${⊢}{H}:{C}\underset{1-1 onto}{⟶}{A}\to {H}:{C}\underset{onto}{⟶}{A}$
62 forn ${⊢}{H}:{C}\underset{onto}{⟶}{A}\to \mathrm{ran}{H}={A}$
63 60 61 62 3syl ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \mathrm{ran}{H}={A}$
64 59 63 sseqtrid ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {H}\left[{b}\right]\subseteq {A}$
65 58 64 fssresd ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left({{F}↾}_{{H}\left[{b}\right]}\right):{H}\left[{b}\right]⟶{B}$
66 fvexd ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {0}_{{G}}\in \mathrm{V}$
67 65 57 66 fdmfifsupp ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {finSupp}_{{0}_{{G}}}\left(\left({{F}↾}_{{H}\left[{b}\right]}\right)\right)$
68 1 48 49 57 65 67 53 gsumf1o ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)={\sum }_{{G}}\left(\left({{F}↾}_{{H}\left[{b}\right]}\right)\circ \left({{H}↾}_{{b}}\right)\right)$
69 df-ima ${⊢}{H}\left[{b}\right]=\mathrm{ran}\left({{H}↾}_{{b}}\right)$
70 69 eqimss2i ${⊢}\mathrm{ran}\left({{H}↾}_{{b}}\right)\subseteq {H}\left[{b}\right]$
71 cores ${⊢}\mathrm{ran}\left({{H}↾}_{{b}}\right)\subseteq {H}\left[{b}\right]\to \left({{F}↾}_{{H}\left[{b}\right]}\right)\circ \left({{H}↾}_{{b}}\right)={F}\circ \left({{H}↾}_{{b}}\right)$
72 70 71 ax-mp ${⊢}\left({{F}↾}_{{H}\left[{b}\right]}\right)\circ \left({{H}↾}_{{b}}\right)={F}\circ \left({{H}↾}_{{b}}\right)$
73 resco ${⊢}{\left({F}\circ {H}\right)↾}_{{b}}={F}\circ \left({{H}↾}_{{b}}\right)$
74 72 73 eqtr4i ${⊢}\left({{F}↾}_{{H}\left[{b}\right]}\right)\circ \left({{H}↾}_{{b}}\right)={\left({F}\circ {H}\right)↾}_{{b}}$
75 74 oveq2i ${⊢}{\sum }_{{G}}\left(\left({{F}↾}_{{H}\left[{b}\right]}\right)\circ \left({{H}↾}_{{b}}\right)\right)={\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)$
76 68 75 syl6eq ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)={\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)$
77 76 eleq1d ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left({\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}↔{\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)$
78 47 77 imbi12d ${⊢}\left(\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\wedge {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left(\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)↔\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)$
79 78 ralbidva ${⊢}\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left(\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {H}\left[{b}\right]\to {\sum }_{{G}}\left({{F}↾}_{{H}\left[{b}\right]}\right)\in {u}\right)↔\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)$
80 36 79 bitr3d ${⊢}\left({\phi }\wedge {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\right)\to \left(\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)$
81 80 rexbidva ${⊢}{\phi }\to \left(\exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({H}\left[{a}\right]\subseteq {z}\to {\sum }_{{G}}\left({{F}↾}_{{z}}\right)\in {u}\right)↔\exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)$
82 18 22 81 3bitr3d ${⊢}{\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)↔\exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)$
83 82 imbi2d ${⊢}{\phi }\to \left(\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)↔\left({x}\in {u}\to \exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)\right)$
84 83 ralbidv ${⊢}{\phi }\to \left(\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)↔\forall {u}\in \mathrm{TopOpen}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {u}\to \exists {a}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)\right)$
85 84 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 {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)↔\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(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)\right)\right)$
86 eqid ${⊢}\mathrm{TopOpen}\left({G}\right)=\mathrm{TopOpen}\left({G}\right)$
87 eqid ${⊢}𝒫{A}\cap \mathrm{Fin}=𝒫{A}\cap \mathrm{Fin}$
88 1 86 87 2 3 4 5 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)$
89 eqid ${⊢}𝒫{C}\cap \mathrm{Fin}=𝒫{C}\cap \mathrm{Fin}$
90 f1dmex ${⊢}\left({H}:{C}\underset{1-1}{⟶}{A}\wedge {A}\in {V}\right)\to {C}\in \mathrm{V}$
91 38 4 90 syl2anc ${⊢}{\phi }\to {C}\in \mathrm{V}$
92 f1of ${⊢}{H}:{C}\underset{1-1 onto}{⟶}{A}\to {H}:{C}⟶{A}$
93 6 92 syl ${⊢}{\phi }\to {H}:{C}⟶{A}$
94 fco ${⊢}\left({F}:{A}⟶{B}\wedge {H}:{C}⟶{A}\right)\to \left({F}\circ {H}\right):{C}⟶{B}$
95 5 93 94 syl2anc ${⊢}{\phi }\to \left({F}\circ {H}\right):{C}⟶{B}$
96 1 86 89 2 3 91 95 eltsms ${⊢}{\phi }\to \left({x}\in \left({G}\mathrm{tsums}\left({F}\circ {H}\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(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in \left(𝒫{C}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({a}\subseteq {b}\to {\sum }_{{G}}\left({\left({F}\circ {H}\right)↾}_{{b}}\right)\in {u}\right)\right)\right)\right)$
97 85 88 96 3bitr4d ${⊢}{\phi }\to \left({x}\in \left({G}\mathrm{tsums}{F}\right)↔{x}\in \left({G}\mathrm{tsums}\left({F}\circ {H}\right)\right)\right)$
98 97 eqrdv ${⊢}{\phi }\to {G}\mathrm{tsums}{F}={G}\mathrm{tsums}\left({F}\circ {H}\right)$