Metamath Proof Explorer

Theorem prodmolem2

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
prodmo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
prodmo.3 
|- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
Assertion prodmolem2 
|- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2 prodmo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodmo.3 
 |-  G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
4 3simpb 
 |-  ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) -> ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) )
5 4 reximi 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) )
6 fveq2 
 |-  ( m = w -> ( ZZ>= ` m ) = ( ZZ>= ` w ) )
7 6 sseq2d 
 |-  ( m = w -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` w ) ) )
8 seqeq1 
 |-  ( m = w -> seq m ( x. , F ) = seq w ( x. , F ) )
9 8 breq1d 
 |-  ( m = w -> ( seq m ( x. , F ) ~~> x <-> seq w ( x. , F ) ~~> x ) )
10 7 9 anbi12d 
 |-  ( m = w -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) <-> ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) ) )
11 10 cbvrexvw 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) <-> E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) )
12 reeanv 
 |-  ( E. w e. ZZ E. m e. NN ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) <-> ( E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) )
13 simprlr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> seq w ( x. , F ) ~~> x )
14 simprll 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A C_ ( ZZ>= ` w ) )
15 uzssz 
 |-  ( ZZ>= ` w ) C_ ZZ
16 zssre 
 |-  ZZ C_ RR
17 15 16 sstri 
 |-  ( ZZ>= ` w ) C_ RR
18 14 17 sstrdi 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A C_ RR )
19 ltso 
 |-  < Or RR
20 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
21 18 19 20 mpisyl 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> < Or A )
22 fzfi 
 |-  ( 1 ... m ) e. Fin
23 ovex 
 |-  ( 1 ... m ) e. _V
24 23 f1oen 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A )
25 24 ad2antll 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( 1 ... m ) ~~ A )
26 25 ensymd 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A ~~ ( 1 ... m ) )
27 enfii 
 |-  ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin )
28 22 26 27 sylancr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> A e. Fin )
29 fz1iso 
 |-  ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
30 21 28 29 syl2anc 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
31 2 ad4ant14 
 |-  ( ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ k e. A ) -> B e. CC )
32 eqid 
 |-  ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / k ]_ B )
33 simplrr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN )
34 simplrl 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> w e. ZZ )
35 simplll 
 |-  ( ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) -> A C_ ( ZZ>= ` w ) )
36 35 adantl 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` w ) )
37 simprlr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
38 simprr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
39 1 31 3 32 33 34 36 37 38 prodmolem2a 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq w ( x. , F ) ~~> ( seq 1 ( x. , G ) ` m ) )
40 39 expr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq w ( x. , F ) ~~> ( seq 1 ( x. , G ) ` m ) ) )
41 40 exlimdv 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq w ( x. , F ) ~~> ( seq 1 ( x. , G ) ` m ) ) )
42 30 41 mpd 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> seq w ( x. , F ) ~~> ( seq 1 ( x. , G ) ` m ) )
43 climuni 
 |-  ( ( seq w ( x. , F ) ~~> x /\ seq w ( x. , F ) ~~> ( seq 1 ( x. , G ) ` m ) ) -> x = ( seq 1 ( x. , G ) ` m ) )
44 13 42 43 syl2anc 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> x = ( seq 1 ( x. , G ) ` m ) )
45 eqeq2 
 |-  ( z = ( seq 1 ( x. , G ) ` m ) -> ( x = z <-> x = ( seq 1 ( x. , G ) ` m ) ) )
46 44 45 syl5ibrcom 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ f : ( 1 ... m ) -1-1-onto-> A ) ) -> ( z = ( seq 1 ( x. , G ) ` m ) -> x = z ) )
47 46 expr 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) ) -> ( f : ( 1 ... m ) -1-1-onto-> A -> ( z = ( seq 1 ( x. , G ) ` m ) -> x = z ) ) )
48 47 impd 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
49 48 exlimdv 
 |-  ( ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
50 49 expimpd 
 |-  ( ( ph /\ ( w e. ZZ /\ m e. NN ) ) -> ( ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
51 50 rexlimdvva 
 |-  ( ph -> ( E. w e. ZZ E. m e. NN ( ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
52 12 51 syl5bir 
 |-  ( ph -> ( ( E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
53 52 expdimp 
 |-  ( ( ph /\ E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
54 11 53 sylan2b 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
55 5 54 sylan2 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )