Metamath Proof Explorer

Theorem summolem2a

Description: Lemma for summo . (Contributed by Mario Carneiro, 3-Apr-2014) (Revised by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses summo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
summo.3 
|- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
summolem2.4 
|- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
summolem2.5 
|- ( ph -> N e. NN )
summolem2.6 
|- ( ph -> M e. ZZ )
summolem2.7 
|- ( ph -> A C_ ( ZZ>= ` M ) )
summolem2.8 
|- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
summolem2.9 
|- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
Assertion summolem2a 
|- ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 summo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2 summo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 summo.3 
 |-  G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
4 summolem2.4 
 |-  H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
5 summolem2.5 
 |-  ( ph -> N e. NN )
6 summolem2.6 
 |-  ( ph -> M e. ZZ )
7 summolem2.7 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
8 summolem2.8 
 |-  ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
9 summolem2.9 
 |-  ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
10 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
11 10 8 hasheqf1od 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = ( # ` A ) )
12 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
13 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
14 5 12 13 3syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
15 11 14 eqtr3d 
 |-  ( ph -> ( # ` A ) = N )
16 15 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` A ) ) = ( 1 ... N ) )
17 isoeq4 
 |-  ( ( 1 ... ( # ` A ) ) = ( 1 ... N ) -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
18 16 17 syl 
 |-  ( ph -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
19 9 18 mpbid 
 |-  ( ph -> K Isom < , < ( ( 1 ... N ) , A ) )
20 isof1o 
 |-  ( K Isom < , < ( ( 1 ... N ) , A ) -> K : ( 1 ... N ) -1-1-onto-> A )
21 19 20 syl 
 |-  ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
22 f1of 
 |-  ( K : ( 1 ... N ) -1-1-onto-> A -> K : ( 1 ... N ) --> A )
23 21 22 syl 
 |-  ( ph -> K : ( 1 ... N ) --> A )
24 nnuz 
 |-  NN = ( ZZ>= ` 1 )
25 5 24 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
26 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
27 25 26 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
28 23 27 ffvelrnd 
 |-  ( ph -> ( K ` N ) e. A )
29 7 28 sseldd 
 |-  ( ph -> ( K ` N ) e. ( ZZ>= ` M ) )
30 7 sselda 
 |-  ( ( ph /\ n e. A ) -> n e. ( ZZ>= ` M ) )
31 f1ocnvfv2 
 |-  ( ( K : ( 1 ... N ) -1-1-onto-> A /\ n e. A ) -> ( K ` ( `' K ` n ) ) = n )
32 21 31 sylan 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( `' K ` n ) ) = n )
33 f1ocnv 
 |-  ( K : ( 1 ... N ) -1-1-onto-> A -> `' K : A -1-1-onto-> ( 1 ... N ) )
34 f1of 
 |-  ( `' K : A -1-1-onto-> ( 1 ... N ) -> `' K : A --> ( 1 ... N ) )
35 21 33 34 3syl 
 |-  ( ph -> `' K : A --> ( 1 ... N ) )
36 35 ffvelrnda 
 |-  ( ( ph /\ n e. A ) -> ( `' K ` n ) e. ( 1 ... N ) )
37 elfzle2 
 |-  ( ( `' K ` n ) e. ( 1 ... N ) -> ( `' K ` n ) <_ N )
38 36 37 syl 
 |-  ( ( ph /\ n e. A ) -> ( `' K ` n ) <_ N )
39 19 adantr 
 |-  ( ( ph /\ n e. A ) -> K Isom < , < ( ( 1 ... N ) , A ) )
40 fzssuz 
 |-  ( 1 ... N ) C_ ( ZZ>= ` 1 )
41 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
42 zssre 
 |-  ZZ C_ RR
43 41 42 sstri 
 |-  ( ZZ>= ` 1 ) C_ RR
44 40 43 sstri 
 |-  ( 1 ... N ) C_ RR
45 ressxr 
 |-  RR C_ RR*
46 44 45 sstri 
 |-  ( 1 ... N ) C_ RR*
47 46 a1i 
 |-  ( ( ph /\ n e. A ) -> ( 1 ... N ) C_ RR* )
48 7 adantr 
 |-  ( ( ph /\ n e. A ) -> A C_ ( ZZ>= ` M ) )
49 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
50 49 42 sstri 
 |-  ( ZZ>= ` M ) C_ RR
51 48 50 sstrdi 
 |-  ( ( ph /\ n e. A ) -> A C_ RR )
52 51 45 sstrdi 
 |-  ( ( ph /\ n e. A ) -> A C_ RR* )
53 27 adantr 
 |-  ( ( ph /\ n e. A ) -> N e. ( 1 ... N ) )
54 leisorel 
 |-  ( ( K Isom < , < ( ( 1 ... N ) , A ) /\ ( ( 1 ... N ) C_ RR* /\ A C_ RR* ) /\ ( ( `' K ` n ) e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) ) -> ( ( `' K ` n ) <_ N <-> ( K ` ( `' K ` n ) ) <_ ( K ` N ) ) )
55 39 47 52 36 53 54 syl122anc 
 |-  ( ( ph /\ n e. A ) -> ( ( `' K ` n ) <_ N <-> ( K ` ( `' K ` n ) ) <_ ( K ` N ) ) )
56 38 55 mpbid 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( `' K ` n ) ) <_ ( K ` N ) )
57 32 56 eqbrtrrd 
 |-  ( ( ph /\ n e. A ) -> n <_ ( K ` N ) )
58 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
59 30 58 syl 
 |-  ( ( ph /\ n e. A ) -> n e. ZZ )
60 eluzelz 
 |-  ( ( K ` N ) e. ( ZZ>= ` M ) -> ( K ` N ) e. ZZ )
61 29 60 syl 
 |-  ( ph -> ( K ` N ) e. ZZ )
62 61 adantr 
 |-  ( ( ph /\ n e. A ) -> ( K ` N ) e. ZZ )
63 eluz 
 |-  ( ( n e. ZZ /\ ( K ` N ) e. ZZ ) -> ( ( K ` N ) e. ( ZZ>= ` n ) <-> n <_ ( K ` N ) ) )
64 59 62 63 syl2anc 
 |-  ( ( ph /\ n e. A ) -> ( ( K ` N ) e. ( ZZ>= ` n ) <-> n <_ ( K ` N ) ) )
65 57 64 mpbird 
 |-  ( ( ph /\ n e. A ) -> ( K ` N ) e. ( ZZ>= ` n ) )
66 elfzuzb 
 |-  ( n e. ( M ... ( K ` N ) ) <-> ( n e. ( ZZ>= ` M ) /\ ( K ` N ) e. ( ZZ>= ` n ) ) )
67 30 65 66 sylanbrc 
 |-  ( ( ph /\ n e. A ) -> n e. ( M ... ( K ` N ) ) )
68 67 ex 
 |-  ( ph -> ( n e. A -> n e. ( M ... ( K ` N ) ) ) )
69 68 ssrdv 
 |-  ( ph -> A C_ ( M ... ( K ` N ) ) )
70 1 2 29 69 fsumcvg 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` ( K ` N ) ) )
71 addid2 
 |-  ( m e. CC -> ( 0 + m ) = m )
72 71 adantl 
 |-  ( ( ph /\ m e. CC ) -> ( 0 + m ) = m )
73 addid1 
 |-  ( m e. CC -> ( m + 0 ) = m )
74 73 adantl 
 |-  ( ( ph /\ m e. CC ) -> ( m + 0 ) = m )
75 addcl 
 |-  ( ( m e. CC /\ x e. CC ) -> ( m + x ) e. CC )
76 75 adantl 
 |-  ( ( ph /\ ( m e. CC /\ x e. CC ) ) -> ( m + x ) e. CC )
77 0cnd 
 |-  ( ph -> 0 e. CC )
78 27 16 eleqtrrd 
 |-  ( ph -> N e. ( 1 ... ( # ` A ) ) )
79 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 0 ) = B )
80 79 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
81 80 2 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
82 81 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
83 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
84 0cn 
 |-  0 e. CC
85 83 84 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
86 82 85 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 0 ) e. CC )
87 86 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> if ( k e. A , B , 0 ) e. CC )
88 87 1 fmptd 
 |-  ( ph -> F : ZZ --> CC )
89 elfzelz 
 |-  ( m e. ( M ... ( K ` ( # ` A ) ) ) -> m e. ZZ )
90 ffvelrn 
 |-  ( ( F : ZZ --> CC /\ m e. ZZ ) -> ( F ` m ) e. CC )
91 88 89 90 syl2an 
 |-  ( ( ph /\ m e. ( M ... ( K ` ( # ` A ) ) ) ) -> ( F ` m ) e. CC )
92 fveqeq2 
 |-  ( k = m -> ( ( F ` k ) = 0 <-> ( F ` m ) = 0 ) )
93 eldifi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ( M ... ( K ` ( # ` A ) ) ) )
94 elfzelz 
 |-  ( k e. ( M ... ( K ` ( # ` A ) ) ) -> k e. ZZ )
95 93 94 syl 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ZZ )
96 eldifn 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> -. k e. A )
97 96 83 syl 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) = 0 )
98 97 84 eqeltrdi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) e. CC )
99 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
100 95 98 99 syl2anc 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
101 100 97 eqtrd 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = 0 )
102 92 101 vtoclga 
 |-  ( m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` m ) = 0 )
103 102 adantl 
 |-  ( ( ph /\ m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) ) -> ( F ` m ) = 0 )
104 isof1o 
 |-  ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> K : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
105 f1of 
 |-  ( K : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> K : ( 1 ... ( # ` A ) ) --> A )
106 9 104 105 3syl 
 |-  ( ph -> K : ( 1 ... ( # ` A ) ) --> A )
107 106 ffvelrnda 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. A )
108 107 iftrued 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) = [_ ( K ` x ) / k ]_ B )
109 7 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
110 109 107 sseldd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ( ZZ>= ` M ) )
111 eluzelz 
 |-  ( ( K ` x ) e. ( ZZ>= ` M ) -> ( K ` x ) e. ZZ )
112 110 111 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ZZ )
113 nfv 
 |-  F/ k ph
114 nfv 
 |-  F/ k ( K ` x ) e. A
115 nfcsb1v 
 |-  F/_ k [_ ( K ` x ) / k ]_ B
116 nfcv 
 |-  F/_ k 0
117 114 115 116 nfif 
 |-  F/_ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 )
118 117 nfel1 
 |-  F/ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC
119 113 118 nfim 
 |-  F/ k ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
120 fvex 
 |-  ( K ` x ) e. _V
121 eleq1 
 |-  ( k = ( K ` x ) -> ( k e. A <-> ( K ` x ) e. A ) )
122 csbeq1a 
 |-  ( k = ( K ` x ) -> B = [_ ( K ` x ) / k ]_ B )
123 121 122 ifbieq1d 
 |-  ( k = ( K ` x ) -> if ( k e. A , B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
124 123 eleq1d 
 |-  ( k = ( K ` x ) -> ( if ( k e. A , B , 0 ) e. CC <-> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) )
125 124 imbi2d 
 |-  ( k = ( K ` x ) -> ( ( ph -> if ( k e. A , B , 0 ) e. CC ) <-> ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) ) )
126 119 120 125 86 vtoclf 
 |-  ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
127 126 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
128 eleq1 
 |-  ( n = ( K ` x ) -> ( n e. A <-> ( K ` x ) e. A ) )
129 csbeq1 
 |-  ( n = ( K ` x ) -> [_ n / k ]_ B = [_ ( K ` x ) / k ]_ B )
130 128 129 ifbieq1d 
 |-  ( n = ( K ` x ) -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
131 nfcv 
 |-  F/_ n if ( k e. A , B , 0 )
132 nfv 
 |-  F/ k n e. A
133 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
134 132 133 116 nfif 
 |-  F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
135 eleq1 
 |-  ( k = n -> ( k e. A <-> n e. A ) )
136 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
137 135 136 ifbieq1d 
 |-  ( k = n -> if ( k e. A , B , 0 ) = if ( n e. A , [_ n / k ]_ B , 0 ) )
138 131 134 137 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
139 1 138 eqtri 
 |-  F = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
140 130 139 fvmptg 
 |-  ( ( ( K ` x ) e. ZZ /\ if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
141 112 127 140 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
142 elfznn 
 |-  ( x e. ( 1 ... ( # ` A ) ) -> x e. NN )
143 108 127 eqeltrrd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> [_ ( K ` x ) / k ]_ B e. CC )
144 fveq2 
 |-  ( n = x -> ( K ` n ) = ( K ` x ) )
145 144 csbeq1d 
 |-  ( n = x -> [_ ( K ` n ) / k ]_ B = [_ ( K ` x ) / k ]_ B )
146 145 4 fvmptg 
 |-  ( ( x e. NN /\ [_ ( K ` x ) / k ]_ B e. CC ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
147 142 143 146 syl2an2 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
148 108 141 147 3eqtr4rd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = ( F ` ( K ` x ) ) )
149 72 74 76 77 9 78 7 91 103 148 seqcoll 
 |-  ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , H ) ` N ) )
150 5 5 jca 
 |-  ( ph -> ( N e. NN /\ N e. NN ) )
151 1 2 3 4 150 8 21 summolem3 
 |-  ( ph -> ( seq 1 ( + , G ) ` N ) = ( seq 1 ( + , H ) ` N ) )
152 149 151 eqtr4d 
 |-  ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , G ) ` N ) )
153 70 152 breqtrd 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )