Metamath Proof Explorer

Theorem seqcoll2

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses seqcoll2.1 
|- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
seqcoll2.1b 
|- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
seqcoll2.c 
|- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
seqcoll2.a 
|- ( ph -> Z e. S )
seqcoll2.2 
|- ( ph -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
seqcoll2.3 
|- ( ph -> A =/= (/) )
seqcoll2.5 
|- ( ph -> A C_ ( M ... N ) )
seqcoll2.6 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
seqcoll2.7 
|- ( ( ph /\ k e. ( ( M ... N ) \ A ) ) -> ( F ` k ) = Z )
seqcoll2.8 
|- ( ( ph /\ n e. ( 1 ... ( # ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )
Assertion seqcoll2 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq 1 ( .+ , H ) ` ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 seqcoll2.1 
 |-  ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )
2 seqcoll2.1b 
 |-  ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )
3 seqcoll2.c 
 |-  ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )
4 seqcoll2.a 
 |-  ( ph -> Z e. S )
5 seqcoll2.2 
 |-  ( ph -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
6 seqcoll2.3 
 |-  ( ph -> A =/= (/) )
7 seqcoll2.5 
 |-  ( ph -> A C_ ( M ... N ) )
8 seqcoll2.6 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
9 seqcoll2.7 
 |-  ( ( ph /\ k e. ( ( M ... N ) \ A ) ) -> ( F ` k ) = Z )
10 seqcoll2.8 
 |-  ( ( ph /\ n e. ( 1 ... ( # ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )
11 fzssuz 
 |-  ( M ... N ) C_ ( ZZ>= ` M )
12 isof1o 
 |-  ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
13 5 12 syl 
 |-  ( ph -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
14 f1of 
 |-  ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> G : ( 1 ... ( # ` A ) ) --> A )
15 13 14 syl 
 |-  ( ph -> G : ( 1 ... ( # ` A ) ) --> A )
16 fzfi 
 |-  ( M ... N ) e. Fin
17 ssfi 
 |-  ( ( ( M ... N ) e. Fin /\ A C_ ( M ... N ) ) -> A e. Fin )
18 16 7 17 sylancr 
 |-  ( ph -> A e. Fin )
19 hasheq0 
 |-  ( A e. Fin -> ( ( # ` A ) = 0 <-> A = (/) ) )
20 18 19 syl 
 |-  ( ph -> ( ( # ` A ) = 0 <-> A = (/) ) )
21 20 necon3bbid 
 |-  ( ph -> ( -. ( # ` A ) = 0 <-> A =/= (/) ) )
22 6 21 mpbird 
 |-  ( ph -> -. ( # ` A ) = 0 )
23 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
24 18 23 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
25 elnn0 
 |-  ( ( # ` A ) e. NN0 <-> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )
26 24 25 sylib 
 |-  ( ph -> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )
27 26 ord 
 |-  ( ph -> ( -. ( # ` A ) e. NN -> ( # ` A ) = 0 ) )
28 22 27 mt3d 
 |-  ( ph -> ( # ` A ) e. NN )
29 nnuz 
 |-  NN = ( ZZ>= ` 1 )
30 28 29 eleqtrdi 
 |-  ( ph -> ( # ` A ) e. ( ZZ>= ` 1 ) )
31 eluzfz2 
 |-  ( ( # ` A ) e. ( ZZ>= ` 1 ) -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
32 30 31 syl 
 |-  ( ph -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
33 15 32 ffvelrnd 
 |-  ( ph -> ( G ` ( # ` A ) ) e. A )
34 7 33 sseldd 
 |-  ( ph -> ( G ` ( # ` A ) ) e. ( M ... N ) )
35 11 34 sseldi 
 |-  ( ph -> ( G ` ( # ` A ) ) e. ( ZZ>= ` M ) )
36 elfzuz3 
 |-  ( ( G ` ( # ` A ) ) e. ( M ... N ) -> N e. ( ZZ>= ` ( G ` ( # ` A ) ) ) )
37 34 36 syl 
 |-  ( ph -> N e. ( ZZ>= ` ( G ` ( # ` A ) ) ) )
38 fzss2 
 |-  ( N e. ( ZZ>= ` ( G ` ( # ` A ) ) ) -> ( M ... ( G ` ( # ` A ) ) ) C_ ( M ... N ) )
39 37 38 syl 
 |-  ( ph -> ( M ... ( G ` ( # ` A ) ) ) C_ ( M ... N ) )
40 39 sselda 
 |-  ( ( ph /\ k e. ( M ... ( G ` ( # ` A ) ) ) ) -> k e. ( M ... N ) )
41 40 8 syldan 
 |-  ( ( ph /\ k e. ( M ... ( G ` ( # ` A ) ) ) ) -> ( F ` k ) e. S )
42 35 41 3 seqcl 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` ( # ` A ) ) ) e. S )
43 peano2uz 
 |-  ( ( G ` ( # ` A ) ) e. ( ZZ>= ` M ) -> ( ( G ` ( # ` A ) ) + 1 ) e. ( ZZ>= ` M ) )
44 35 43 syl 
 |-  ( ph -> ( ( G ` ( # ` A ) ) + 1 ) e. ( ZZ>= ` M ) )
45 fzss1 
 |-  ( ( ( G ` ( # ` A ) ) + 1 ) e. ( ZZ>= ` M ) -> ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) C_ ( M ... N ) )
46 44 45 syl 
 |-  ( ph -> ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) C_ ( M ... N ) )
47 46 sselda 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> k e. ( M ... N ) )
48 eluzelre 
 |-  ( ( G ` ( # ` A ) ) e. ( ZZ>= ` M ) -> ( G ` ( # ` A ) ) e. RR )
49 35 48 syl 
 |-  ( ph -> ( G ` ( # ` A ) ) e. RR )
50 49 adantr 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( G ` ( # ` A ) ) e. RR )
51 peano2re 
 |-  ( ( G ` ( # ` A ) ) e. RR -> ( ( G ` ( # ` A ) ) + 1 ) e. RR )
52 50 51 syl 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( ( G ` ( # ` A ) ) + 1 ) e. RR )
53 elfzelz 
 |-  ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) -> k e. ZZ )
54 53 zred 
 |-  ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) -> k e. RR )
55 54 adantl 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> k e. RR )
56 50 ltp1d 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( G ` ( # ` A ) ) < ( ( G ` ( # ` A ) ) + 1 ) )
57 elfzle1 
 |-  ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) -> ( ( G ` ( # ` A ) ) + 1 ) <_ k )
58 57 adantl 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( ( G ` ( # ` A ) ) + 1 ) <_ k )
59 50 52 55 56 58 ltletrd 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( G ` ( # ` A ) ) < k )
60 13 adantr 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> G : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
61 f1ocnv 
 |-  ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) )
62 60 61 syl 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) )
63 f1of 
 |-  ( `' G : A -1-1-onto-> ( 1 ... ( # ` A ) ) -> `' G : A --> ( 1 ... ( # ` A ) ) )
64 62 63 syl 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> `' G : A --> ( 1 ... ( # ` A ) ) )
65 simprr 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> k e. A )
66 64 65 ffvelrnd 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( `' G ` k ) e. ( 1 ... ( # ` A ) ) )
67 elfzelz 
 |-  ( ( `' G ` k ) e. ( 1 ... ( # ` A ) ) -> ( `' G ` k ) e. ZZ )
68 66 67 syl 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( `' G ` k ) e. ZZ )
69 68 zred 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( `' G ` k ) e. RR )
70 24 adantr 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( # ` A ) e. NN0 )
71 70 nn0red 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( # ` A ) e. RR )
72 elfzle2 
 |-  ( ( `' G ` k ) e. ( 1 ... ( # ` A ) ) -> ( `' G ` k ) <_ ( # ` A ) )
73 66 72 syl 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( `' G ` k ) <_ ( # ` A ) )
74 69 71 73 lensymd 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> -. ( # ` A ) < ( `' G ` k ) )
75 5 adantr 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
76 32 adantr 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( # ` A ) e. ( 1 ... ( # ` A ) ) )
77 isorel 
 |-  ( ( G Isom < , < ( ( 1 ... ( # ` A ) ) , A ) /\ ( ( # ` A ) e. ( 1 ... ( # ` A ) ) /\ ( `' G ` k ) e. ( 1 ... ( # ` A ) ) ) ) -> ( ( # ` A ) < ( `' G ` k ) <-> ( G ` ( # ` A ) ) < ( G ` ( `' G ` k ) ) ) )
78 75 76 66 77 syl12anc 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( ( # ` A ) < ( `' G ` k ) <-> ( G ` ( # ` A ) ) < ( G ` ( `' G ` k ) ) ) )
79 f1ocnvfv2 
 |-  ( ( G : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ k e. A ) -> ( G ` ( `' G ` k ) ) = k )
80 60 65 79 syl2anc 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( G ` ( `' G ` k ) ) = k )
81 80 breq2d 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( ( G ` ( # ` A ) ) < ( G ` ( `' G ` k ) ) <-> ( G ` ( # ` A ) ) < k ) )
82 78 81 bitrd 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> ( ( # ` A ) < ( `' G ` k ) <-> ( G ` ( # ` A ) ) < k ) )
83 74 82 mtbid 
 |-  ( ( ph /\ ( k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) /\ k e. A ) ) -> -. ( G ` ( # ` A ) ) < k )
84 83 expr 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( k e. A -> -. ( G ` ( # ` A ) ) < k ) )
85 59 84 mt2d 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> -. k e. A )
86 47 85 eldifd 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> k e. ( ( M ... N ) \ A ) )
87 86 9 syldan 
 |-  ( ( ph /\ k e. ( ( ( G ` ( # ` A ) ) + 1 ) ... N ) ) -> ( F ` k ) = Z )
88 2 35 37 42 87 seqid2 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` ( # ` A ) ) ) = ( seq M ( .+ , F ) ` N ) )
89 7 11 sstrdi 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
90 39 ssdifd 
 |-  ( ph -> ( ( M ... ( G ` ( # ` A ) ) ) \ A ) C_ ( ( M ... N ) \ A ) )
91 90 sselda 
 |-  ( ( ph /\ k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) ) -> k e. ( ( M ... N ) \ A ) )
92 91 9 syldan 
 |-  ( ( ph /\ k e. ( ( M ... ( G ` ( # ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )
93 1 2 3 4 5 32 89 41 92 10 seqcoll 
 |-  ( ph -> ( seq M ( .+ , F ) ` ( G ` ( # ` A ) ) ) = ( seq 1 ( .+ , H ) ` ( # ` A ) ) )
94 88 93 eqtr3d 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq 1 ( .+ , H ) ` ( # ` A ) ) )