Metamath Proof Explorer

Theorem summolem3

Description: Lemma for summo . (Contributed by Mario Carneiro, 29-Mar-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 )
summolem3.4 
|- H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
summolem3.5 
|- ( ph -> ( M e. NN /\ N e. NN ) )
summolem3.6 
|- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
summolem3.7 
|- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
Assertion summolem3 
|- ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` 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 summolem3.4 
 |-  H = ( n e. NN |-> [_ ( K ` n ) / k ]_ B )
5 summolem3.5 
 |-  ( ph -> ( M e. NN /\ N e. NN ) )
6 summolem3.6 
 |-  ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
7 summolem3.7 
 |-  ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
8 addcl 
 |-  ( ( m e. CC /\ j e. CC ) -> ( m + j ) e. CC )
9 8 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m + j ) e. CC )
10 addcom 
 |-  ( ( m e. CC /\ j e. CC ) -> ( m + j ) = ( j + m ) )
11 10 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m + j ) = ( j + m ) )
12 addass 
 |-  ( ( m e. CC /\ j e. CC /\ y e. CC ) -> ( ( m + j ) + y ) = ( m + ( j + y ) ) )
13 12 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC /\ y e. CC ) ) -> ( ( m + j ) + y ) = ( m + ( j + y ) ) )
14 5 simpld 
 |-  ( ph -> M e. NN )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
17 ssidd 
 |-  ( ph -> CC C_ CC )
18 f1ocnv 
 |-  ( f : ( 1 ... M ) -1-1-onto-> A -> `' f : A -1-1-onto-> ( 1 ... M ) )
19 6 18 syl 
 |-  ( ph -> `' f : A -1-1-onto-> ( 1 ... M ) )
20 f1oco 
 |-  ( ( `' f : A -1-1-onto-> ( 1 ... M ) /\ K : ( 1 ... N ) -1-1-onto-> A ) -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
21 19 7 20 syl2anc 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
22 ovex 
 |-  ( 1 ... N ) e. _V
23 22 f1oen 
 |-  ( ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) -> ( 1 ... N ) ~~ ( 1 ... M ) )
24 21 23 syl 
 |-  ( ph -> ( 1 ... N ) ~~ ( 1 ... M ) )
25 fzfi 
 |-  ( 1 ... N ) e. Fin
26 fzfi 
 |-  ( 1 ... M ) e. Fin
27 hashen 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... M ) e. Fin ) -> ( ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) <-> ( 1 ... N ) ~~ ( 1 ... M ) ) )
28 25 26 27 mp2an 
 |-  ( ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) <-> ( 1 ... N ) ~~ ( 1 ... M ) )
29 24 28 sylibr 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) )
30 5 simprd 
 |-  ( ph -> N e. NN )
31 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
32 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
33 30 31 32 3syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
34 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
35 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
36 14 34 35 3syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
37 29 33 36 3eqtr3rd 
 |-  ( ph -> M = N )
38 37 oveq2d 
 |-  ( ph -> ( 1 ... M ) = ( 1 ... N ) )
39 38 f1oeq2d 
 |-  ( ph -> ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) ) )
40 21 39 mpbird 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
41 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
42 41 csbeq1d 
 |-  ( n = m -> [_ ( f ` n ) / k ]_ B = [_ ( f ` m ) / k ]_ B )
43 elfznn 
 |-  ( m e. ( 1 ... M ) -> m e. NN )
44 43 adantl 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> m e. NN )
45 f1of 
 |-  ( f : ( 1 ... M ) -1-1-onto-> A -> f : ( 1 ... M ) --> A )
46 6 45 syl 
 |-  ( ph -> f : ( 1 ... M ) --> A )
47 46 ffvelcdmda 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( f ` m ) e. A )
48 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
49 48 adantr 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> A. k e. A B e. CC )
50 nfcsb1v 
 |-  F/_ k [_ ( f ` m ) / k ]_ B
51 50 nfel1 
 |-  F/ k [_ ( f ` m ) / k ]_ B e. CC
52 csbeq1a 
 |-  ( k = ( f ` m ) -> B = [_ ( f ` m ) / k ]_ B )
53 52 eleq1d 
 |-  ( k = ( f ` m ) -> ( B e. CC <-> [_ ( f ` m ) / k ]_ B e. CC ) )
54 51 53 rspc 
 |-  ( ( f ` m ) e. A -> ( A. k e. A B e. CC -> [_ ( f ` m ) / k ]_ B e. CC ) )
55 47 49 54 sylc 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> [_ ( f ` m ) / k ]_ B e. CC )
56 3 42 44 55 fvmptd3 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( G ` m ) = [_ ( f ` m ) / k ]_ B )
57 56 55 eqeltrd 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( G ` m ) e. CC )
58 38 f1oeq2d 
 |-  ( ph -> ( K : ( 1 ... M ) -1-1-onto-> A <-> K : ( 1 ... N ) -1-1-onto-> A ) )
59 7 58 mpbird 
 |-  ( ph -> K : ( 1 ... M ) -1-1-onto-> A )
60 f1of 
 |-  ( K : ( 1 ... M ) -1-1-onto-> A -> K : ( 1 ... M ) --> A )
61 59 60 syl 
 |-  ( ph -> K : ( 1 ... M ) --> A )
62 fvco3 
 |-  ( ( K : ( 1 ... M ) --> A /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
63 61 62 sylan 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
64 63 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( ( `' f o. K ) ` i ) ) = ( f ` ( `' f ` ( K ` i ) ) ) )
65 6 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> f : ( 1 ... M ) -1-1-onto-> A )
66 61 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) e. A )
67 f1ocnvfv2 
 |-  ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( K ` i ) e. A ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
68 65 66 67 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
69 64 68 eqtr2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) = ( f ` ( ( `' f o. K ) ` i ) ) )
70 69 csbeq1d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> [_ ( K ` i ) / k ]_ B = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
71 70 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( _I ` [_ ( K ` i ) / k ]_ B ) = ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) )
72 elfznn 
 |-  ( i e. ( 1 ... M ) -> i e. NN )
73 72 adantl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> i e. NN )
74 fveq2 
 |-  ( n = i -> ( K ` n ) = ( K ` i ) )
75 74 csbeq1d 
 |-  ( n = i -> [_ ( K ` n ) / k ]_ B = [_ ( K ` i ) / k ]_ B )
76 75 4 fvmpti 
 |-  ( i e. NN -> ( H ` i ) = ( _I ` [_ ( K ` i ) / k ]_ B ) )
77 73 76 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = ( _I ` [_ ( K ` i ) / k ]_ B ) )
78 f1of 
 |-  ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
79 40 78 syl 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
80 79 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) e. ( 1 ... M ) )
81 elfznn 
 |-  ( ( ( `' f o. K ) ` i ) e. ( 1 ... M ) -> ( ( `' f o. K ) ` i ) e. NN )
82 fveq2 
 |-  ( n = ( ( `' f o. K ) ` i ) -> ( f ` n ) = ( f ` ( ( `' f o. K ) ` i ) ) )
83 82 csbeq1d 
 |-  ( n = ( ( `' f o. K ) ` i ) -> [_ ( f ` n ) / k ]_ B = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
84 83 3 fvmpti 
 |-  ( ( ( `' f o. K ) ` i ) e. NN -> ( G ` ( ( `' f o. K ) ` i ) ) = ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) )
85 80 81 84 3syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( ( `' f o. K ) ` i ) ) = ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) )
86 71 77 85 3eqtr4d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = ( G ` ( ( `' f o. K ) ` i ) ) )
87 9 11 13 16 17 40 57 86 seqf1o 
 |-  ( ph -> ( seq 1 ( + , H ) ` M ) = ( seq 1 ( + , G ) ` M ) )
88 37 fveq2d 
 |-  ( ph -> ( seq 1 ( + , H ) ` M ) = ( seq 1 ( + , H ) ` N ) )
89 87 88 eqtr3d 
 |-  ( ph -> ( seq 1 ( + , G ) ` M ) = ( seq 1 ( + , H ) ` N ) )