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=BaseG
tsmsf1o.1 φGCMnd
tsmsf1o.2 φGTopSp
tsmsf1o.a φAV
tsmsf1o.f φF:AB
tsmsf1o.s φH:C1-1 ontoA
Assertion tsmsf1o φGtsumsF=GtsumsFH

Proof

Step Hyp Ref Expression
1 tsmsf1o.b B=BaseG
2 tsmsf1o.1 φGCMnd
3 tsmsf1o.2 φGTopSp
4 tsmsf1o.a φAV
5 tsmsf1o.f φF:AB
6 tsmsf1o.s φH:C1-1 ontoA
7 f1opwfi H:C1-1 ontoAa𝒫CFinHa:𝒫CFin1-1 onto𝒫AFin
8 6 7 syl φa𝒫CFinHa:𝒫CFin1-1 onto𝒫AFin
9 f1of a𝒫CFinHa:𝒫CFin1-1 onto𝒫AFina𝒫CFinHa:𝒫CFin𝒫AFin
10 8 9 syl φa𝒫CFinHa:𝒫CFin𝒫AFin
11 eqid a𝒫CFinHa=a𝒫CFinHa
12 11 fmpt a𝒫CFinHa𝒫AFina𝒫CFinHa:𝒫CFin𝒫AFin
13 10 12 sylibr φa𝒫CFinHa𝒫AFin
14 sseq1 y=HayzHaz
15 14 imbi1d y=HayzGFzuHazGFzu
16 15 ralbidv y=Haz𝒫AFinyzGFzuz𝒫AFinHazGFzu
17 11 16 rexrnmptw a𝒫CFinHa𝒫AFinyrana𝒫CFinHaz𝒫AFinyzGFzua𝒫CFinz𝒫AFinHazGFzu
18 13 17 syl φyrana𝒫CFinHaz𝒫AFinyzGFzua𝒫CFinz𝒫AFinHazGFzu
19 f1ofo a𝒫CFinHa:𝒫CFin1-1 onto𝒫AFina𝒫CFinHa:𝒫CFinonto𝒫AFin
20 forn a𝒫CFinHa:𝒫CFinonto𝒫AFinrana𝒫CFinHa=𝒫AFin
21 8 19 20 3syl φrana𝒫CFinHa=𝒫AFin
22 21 rexeqdv φyrana𝒫CFinHaz𝒫AFinyzGFzuy𝒫AFinz𝒫AFinyzGFzu
23 imaeq2 a=bHa=Hb
24 23 cbvmptv a𝒫CFinHa=b𝒫CFinHb
25 24 fmpt b𝒫CFinHb𝒫AFina𝒫CFinHa:𝒫CFin𝒫AFin
26 10 25 sylibr φb𝒫CFinHb𝒫AFin
27 sseq2 z=HbHazHaHb
28 reseq2 z=HbFz=FHb
29 28 oveq2d z=HbGFz=GFHb
30 29 eleq1d z=HbGFzuGFHbu
31 27 30 imbi12d z=HbHazGFzuHaHbGFHbu
32 24 31 ralrnmptw b𝒫CFinHb𝒫AFinzrana𝒫CFinHaHazGFzub𝒫CFinHaHbGFHbu
33 26 32 syl φzrana𝒫CFinHaHazGFzub𝒫CFinHaHbGFHbu
34 21 raleqdv φzrana𝒫CFinHaHazGFzuz𝒫AFinHazGFzu
35 33 34 bitr3d φb𝒫CFinHaHbGFHbuz𝒫AFinHazGFzu
36 35 adantr φa𝒫CFinb𝒫CFinHaHbGFHbuz𝒫AFinHazGFzu
37 f1of1 H:C1-1 ontoAH:C1-1A
38 6 37 syl φH:C1-1A
39 38 ad2antrr φa𝒫CFinb𝒫CFinH:C1-1A
40 elfpw a𝒫CFinaCaFin
41 40 simplbi a𝒫CFinaC
42 41 ad2antlr φa𝒫CFinb𝒫CFinaC
43 elfpw b𝒫CFinbCbFin
44 43 simplbi b𝒫CFinbC
45 44 adantl φa𝒫CFinb𝒫CFinbC
46 f1imass H:C1-1AaCbCHaHbab
47 39 42 45 46 syl12anc φa𝒫CFinb𝒫CFinHaHbab
48 eqid 0G=0G
49 2 ad2antrr φa𝒫CFinb𝒫CFinGCMnd
50 elinel2 b𝒫CFinbFin
51 50 adantl φa𝒫CFinb𝒫CFinbFin
52 f1ores H:C1-1AbCHb:b1-1 ontoHb
53 39 45 52 syl2anc φa𝒫CFinb𝒫CFinHb:b1-1 ontoHb
54 f1ofo Hb:b1-1 ontoHbHb:bontoHb
55 53 54 syl φa𝒫CFinb𝒫CFinHb:bontoHb
56 fofi bFinHb:bontoHbHbFin
57 51 55 56 syl2anc φa𝒫CFinb𝒫CFinHbFin
58 5 ad2antrr φa𝒫CFinb𝒫CFinF:AB
59 imassrn HbranH
60 6 ad2antrr φa𝒫CFinb𝒫CFinH:C1-1 ontoA
61 f1ofo H:C1-1 ontoAH:ContoA
62 forn H:ContoAranH=A
63 60 61 62 3syl φa𝒫CFinb𝒫CFinranH=A
64 59 63 sseqtrid φa𝒫CFinb𝒫CFinHbA
65 58 64 fssresd φa𝒫CFinb𝒫CFinFHb:HbB
66 fvexd φa𝒫CFinb𝒫CFin0GV
67 65 57 66 fdmfifsupp φa𝒫CFinb𝒫CFinfinSupp0GFHb
68 1 48 49 57 65 67 53 gsumf1o φa𝒫CFinb𝒫CFinGFHb=GFHbHb
69 df-ima Hb=ranHb
70 69 eqimss2i ranHbHb
71 cores ranHbHbFHbHb=FHb
72 70 71 ax-mp FHbHb=FHb
73 resco FHb=FHb
74 72 73 eqtr4i FHbHb=FHb
75 74 oveq2i GFHbHb=GFHb
76 68 75 eqtrdi φa𝒫CFinb𝒫CFinGFHb=GFHb
77 76 eleq1d φa𝒫CFinb𝒫CFinGFHbuGFHbu
78 47 77 imbi12d φa𝒫CFinb𝒫CFinHaHbGFHbuabGFHbu
79 78 ralbidva φa𝒫CFinb𝒫CFinHaHbGFHbub𝒫CFinabGFHbu
80 36 79 bitr3d φa𝒫CFinz𝒫AFinHazGFzub𝒫CFinabGFHbu
81 80 rexbidva φa𝒫CFinz𝒫AFinHazGFzua𝒫CFinb𝒫CFinabGFHbu
82 18 22 81 3bitr3d φy𝒫AFinz𝒫AFinyzGFzua𝒫CFinb𝒫CFinabGFHbu
83 82 imbi2d φxuy𝒫AFinz𝒫AFinyzGFzuxua𝒫CFinb𝒫CFinabGFHbu
84 83 ralbidv φuTopOpenGxuy𝒫AFinz𝒫AFinyzGFzuuTopOpenGxua𝒫CFinb𝒫CFinabGFHbu
85 84 anbi2d φxBuTopOpenGxuy𝒫AFinz𝒫AFinyzGFzuxBuTopOpenGxua𝒫CFinb𝒫CFinabGFHbu
86 eqid TopOpenG=TopOpenG
87 eqid 𝒫AFin=𝒫AFin
88 1 86 87 2 3 4 5 eltsms φxGtsumsFxBuTopOpenGxuy𝒫AFinz𝒫AFinyzGFzu
89 eqid 𝒫CFin=𝒫CFin
90 f1dmex H:C1-1AAVCV
91 38 4 90 syl2anc φCV
92 f1of H:C1-1 ontoAH:CA
93 6 92 syl φH:CA
94 fco F:ABH:CAFH:CB
95 5 93 94 syl2anc φFH:CB
96 1 86 89 2 3 91 95 eltsms φxGtsumsFHxBuTopOpenGxua𝒫CFinb𝒫CFinabGFHbu
97 85 88 96 3bitr4d φxGtsumsFxGtsumsFH
98 97 eqrdv φGtsumsF=GtsumsFH