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 = Base G
tsmsf1o.1 φ G CMnd
tsmsf1o.2 φ G TopSp
tsmsf1o.a φ A V
tsmsf1o.f φ F : A B
tsmsf1o.s φ H : C 1-1 onto A
Assertion tsmsf1o φ G tsums F = G tsums F H

Proof

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