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 93 elfzelzd 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ZZ )
95 eldifn 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> -. k e. A )
96 95 83 syl 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) = 0 )
97 96 84 eqeltrdi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 0 ) e. CC )
98 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
99 94 97 98 syl2anc 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
100 99 96 eqtrd 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = 0 )
101 92 100 vtoclga 
 |-  ( m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` m ) = 0 )
102 101 adantl 
 |-  ( ( ph /\ m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) ) -> ( F ` m ) = 0 )
103 isof1o 
 |-  ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> K : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
104 f1of 
 |-  ( K : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> K : ( 1 ... ( # ` A ) ) --> A )
105 9 103 104 3syl 
 |-  ( ph -> K : ( 1 ... ( # ` A ) ) --> A )
106 105 ffvelrnda 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. A )
107 106 iftrued 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) = [_ ( K ` x ) / k ]_ B )
108 7 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> A C_ ( ZZ>= ` M ) )
109 108 106 sseldd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ( ZZ>= ` M ) )
110 eluzelz 
 |-  ( ( K ` x ) e. ( ZZ>= ` M ) -> ( K ` x ) e. ZZ )
111 109 110 syl 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ZZ )
112 nfv 
 |-  F/ k ph
113 nfv 
 |-  F/ k ( K ` x ) e. A
114 nfcsb1v 
 |-  F/_ k [_ ( K ` x ) / k ]_ B
115 nfcv 
 |-  F/_ k 0
116 113 114 115 nfif 
 |-  F/_ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 )
117 116 nfel1 
 |-  F/ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC
118 112 117 nfim 
 |-  F/ k ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
119 fvex 
 |-  ( K ` x ) e. _V
120 eleq1 
 |-  ( k = ( K ` x ) -> ( k e. A <-> ( K ` x ) e. A ) )
121 csbeq1a 
 |-  ( k = ( K ` x ) -> B = [_ ( K ` x ) / k ]_ B )
122 120 121 ifbieq1d 
 |-  ( k = ( K ` x ) -> if ( k e. A , B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
123 122 eleq1d 
 |-  ( k = ( K ` x ) -> ( if ( k e. A , B , 0 ) e. CC <-> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC ) )
124 123 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 ) ) )
125 118 119 124 86 vtoclf 
 |-  ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
126 125 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) e. CC )
127 eleq1 
 |-  ( n = ( K ` x ) -> ( n e. A <-> ( K ` x ) e. A ) )
128 csbeq1 
 |-  ( n = ( K ` x ) -> [_ n / k ]_ B = [_ ( K ` x ) / k ]_ B )
129 127 128 ifbieq1d 
 |-  ( n = ( K ` x ) -> if ( n e. A , [_ n / k ]_ B , 0 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
130 nfcv 
 |-  F/_ n if ( k e. A , B , 0 )
131 nfv 
 |-  F/ k n e. A
132 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
133 131 132 115 nfif 
 |-  F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
134 eleq1 
 |-  ( k = n -> ( k e. A <-> n e. A ) )
135 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
136 134 135 ifbieq1d 
 |-  ( k = n -> if ( k e. A , B , 0 ) = if ( n e. A , [_ n / k ]_ B , 0 ) )
137 130 133 136 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
138 1 137 eqtri 
 |-  F = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
139 129 138 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 ) )
140 111 126 139 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 0 ) )
141 elfznn 
 |-  ( x e. ( 1 ... ( # ` A ) ) -> x e. NN )
142 107 126 eqeltrrd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> [_ ( K ` x ) / k ]_ B e. CC )
143 fveq2 
 |-  ( n = x -> ( K ` n ) = ( K ` x ) )
144 143 csbeq1d 
 |-  ( n = x -> [_ ( K ` n ) / k ]_ B = [_ ( K ` x ) / k ]_ B )
145 144 4 fvmptg 
 |-  ( ( x e. NN /\ [_ ( K ` x ) / k ]_ B e. CC ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
146 141 142 145 syl2an2 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
147 107 140 146 3eqtr4rd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = ( F ` ( K ` x ) ) )
148 72 74 76 77 9 78 7 91 102 147 seqcoll 
 |-  ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , H ) ` N ) )
149 5 5 jca 
 |-  ( ph -> ( N e. NN /\ N e. NN ) )
150 1 2 3 4 149 8 21 summolem3 
 |-  ( ph -> ( seq 1 ( + , G ) ` N ) = ( seq 1 ( + , H ) ` N ) )
151 148 150 eqtr4d 
 |-  ( ph -> ( seq M ( + , F ) ` ( K ` N ) ) = ( seq 1 ( + , G ) ` N ) )
152 70 151 breqtrd 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq 1 ( + , G ) ` N ) )