Metamath Proof Explorer

Theorem summolem2

Description: Lemma for summo . (Contributed by Mario Carneiro, 3-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 )
Assertion summolem2 
|- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )

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 fveq2 
 |-  ( m = j -> ( ZZ>= ` m ) = ( ZZ>= ` j ) )
5 4 sseq2d 
 |-  ( m = j -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` j ) ) )
6 seqeq1 
 |-  ( m = j -> seq m ( + , F ) = seq j ( + , F ) )
7 6 breq1d 
 |-  ( m = j -> ( seq m ( + , F ) ~~> x <-> seq j ( + , F ) ~~> x ) )
8 5 7 anbi12d 
 |-  ( m = j -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) )
9 8 cbvrexvw 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> E. j e. ZZ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) )
10 simplrr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> seq j ( + , F ) ~~> x )
11 simplrl 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A C_ ( ZZ>= ` j ) )
12 uzssz 
 |-  ( ZZ>= ` j ) C_ ZZ
13 zssre 
 |-  ZZ C_ RR
14 12 13 sstri 
 |-  ( ZZ>= ` j ) C_ RR
15 11 14 sstrdi 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A C_ RR )
16 ltso 
 |-  < Or RR
17 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
18 15 16 17 mpisyl 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> < Or A )
19 fzfi 
 |-  ( 1 ... m ) e. Fin
20 ovex 
 |-  ( 1 ... m ) e. _V
21 20 f1oen 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A )
22 21 ad2antll 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( 1 ... m ) ~~ A )
23 22 ensymd 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A ~~ ( 1 ... m ) )
24 enfii 
 |-  ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin )
25 19 23 24 sylancr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A e. Fin )
26 fz1iso 
 |-  ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
27 18 25 26 syl2anc 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
28 2 ad5ant15 
 |-  ( ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ k e. A ) -> B e. CC )
29 eqid 
 |-  ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) = ( n e. NN |-> [_ ( g ` n ) / k ]_ B )
30 simprll 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN )
31 simpllr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> j e. ZZ )
32 simplrl 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` j ) )
33 simprlr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
34 simprr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
35 1 28 3 29 30 31 32 33 34 summolem2a 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq j ( + , F ) ~~> ( seq 1 ( + , G ) ` m ) )
36 35 expr 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq j ( + , F ) ~~> ( seq 1 ( + , G ) ` m ) ) )
37 36 exlimdv 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq j ( + , F ) ~~> ( seq 1 ( + , G ) ` m ) ) )
38 27 37 mpd 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> seq j ( + , F ) ~~> ( seq 1 ( + , G ) ` m ) )
39 climuni 
 |-  ( ( seq j ( + , F ) ~~> x /\ seq j ( + , F ) ~~> ( seq 1 ( + , G ) ` m ) ) -> x = ( seq 1 ( + , G ) ` m ) )
40 10 38 39 syl2anc 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> x = ( seq 1 ( + , G ) ` m ) )
41 40 anassrs 
 |-  ( ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> x = ( seq 1 ( + , G ) ` m ) )
42 eqeq2 
 |-  ( y = ( seq 1 ( + , G ) ` m ) -> ( x = y <-> x = ( seq 1 ( + , G ) ` m ) ) )
43 41 42 syl5ibrcom 
 |-  ( ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( y = ( seq 1 ( + , G ) ` m ) -> x = y ) )
44 43 expimpd 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
45 44 exlimdv 
 |-  ( ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
46 45 rexlimdva 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
47 46 r19.29an 
 |-  ( ( ph /\ E. j e. ZZ ( A C_ ( ZZ>= ` j ) /\ seq j ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
48 9 47 sylan2b 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )