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

Proof

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