Metamath Proof Explorer

Theorem ulmshftlem

Description: Lemma for ulmshft . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmshft.z 
|- Z = ( ZZ>= ` M )
ulmshft.w 
|- W = ( ZZ>= ` ( M + K ) )
ulmshft.m 
|- ( ph -> M e. ZZ )
ulmshft.k 
|- ( ph -> K e. ZZ )
ulmshft.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
ulmshft.h 
|- ( ph -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
Assertion ulmshftlem 
|- ( ph -> ( F ( ~~>u ` S ) G -> H ( ~~>u ` S ) G ) )

Proof

Step Hyp Ref Expression
1 ulmshft.z 
 |-  Z = ( ZZ>= ` M )
2 ulmshft.w 
 |-  W = ( ZZ>= ` ( M + K ) )
3 ulmshft.m 
 |-  ( ph -> M e. ZZ )
4 ulmshft.k 
 |-  ( ph -> K e. ZZ )
5 ulmshft.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
6 ulmshft.h 
 |-  ( ph -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
7 3 ad2antrr 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> M e. ZZ )
8 5 ad2antrr 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> F : Z --> ( CC ^m S ) )
9 eqidd 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ ( m e. Z /\ z e. S ) ) -> ( ( F ` m ) ` z ) = ( ( F ` m ) ` z ) )
10 eqidd 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
11 simplr 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> F ( ~~>u ` S ) G )
12 simpr 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> x e. RR+ )
13 1 7 8 9 10 11 12 ulmi 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> E. i e. Z A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x )
14 simpr 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> i e. Z )
15 14 1 eleqtrdi 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
16 4 ad3antrrr 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> K e. ZZ )
17 eluzadd 
 |-  ( ( i e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( i + K ) e. ( ZZ>= ` ( M + K ) ) )
18 15 16 17 syl2anc 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> ( i + K ) e. ( ZZ>= ` ( M + K ) ) )
19 18 2 eleqtrrdi 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> ( i + K ) e. W )
20 eluzelz 
 |-  ( i e. ( ZZ>= ` M ) -> i e. ZZ )
21 15 20 syl 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> i e. ZZ )
22 21 adantr 
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) /\ k e. ( ZZ>= ` ( i + K ) ) ) -> i e. ZZ )
23 4 adantr 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> K e. ZZ )
24 23 ad3antrrr 
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) /\ k e. ( ZZ>= ` ( i + K ) ) ) -> K e. ZZ )
25 simpr 
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) /\ k e. ( ZZ>= ` ( i + K ) ) ) -> k e. ( ZZ>= ` ( i + K ) ) )
26 eluzsub 
 |-  ( ( i e. ZZ /\ K e. ZZ /\ k e. ( ZZ>= ` ( i + K ) ) ) -> ( k - K ) e. ( ZZ>= ` i ) )
27 22 24 25 26 syl3anc 
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) /\ k e. ( ZZ>= ` ( i + K ) ) ) -> ( k - K ) e. ( ZZ>= ` i ) )
28 fveq2 
 |-  ( m = ( k - K ) -> ( F ` m ) = ( F ` ( k - K ) ) )
29 28 fveq1d 
 |-  ( m = ( k - K ) -> ( ( F ` m ) ` z ) = ( ( F ` ( k - K ) ) ` z ) )
30 29 fvoveq1d 
 |-  ( m = ( k - K ) -> ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) )
31 30 breq1d 
 |-  ( m = ( k - K ) -> ( ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x <-> ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
32 31 ralbidv 
 |-  ( m = ( k - K ) -> ( A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
33 32 rspcv 
 |-  ( ( k - K ) e. ( ZZ>= ` i ) -> ( A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x -> A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
34 27 33 syl 
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) /\ k e. ( ZZ>= ` ( i + K ) ) ) -> ( A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x -> A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
35 34 ralrimdva 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> ( A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x -> A. k e. ( ZZ>= ` ( i + K ) ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
36 fveq2 
 |-  ( j = ( i + K ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( i + K ) ) )
37 36 raleqdv 
 |-  ( j = ( i + K ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x <-> A. k e. ( ZZ>= ` ( i + K ) ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
38 37 rspcev 
 |-  ( ( ( i + K ) e. W /\ A. k e. ( ZZ>= ` ( i + K ) ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) -> E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x )
39 19 35 38 syl6an 
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) /\ i e. Z ) -> ( A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x -> E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
40 39 rexlimdva 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> ( E. i e. Z A. m e. ( ZZ>= ` i ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( G ` z ) ) ) < x -> E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
41 13 40 mpd 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ x e. RR+ ) -> E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x )
42 41 ralrimiva 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x )
43 3 4 zaddcld 
 |-  ( ph -> ( M + K ) e. ZZ )
44 43 adantr 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> ( M + K ) e. ZZ )
45 5 adantr 
 |-  ( ( ph /\ n e. W ) -> F : Z --> ( CC ^m S ) )
46 3 adantr 
 |-  ( ( ph /\ n e. W ) -> M e. ZZ )
47 4 adantr 
 |-  ( ( ph /\ n e. W ) -> K e. ZZ )
48 simpr 
 |-  ( ( ph /\ n e. W ) -> n e. W )
49 48 2 eleqtrdi 
 |-  ( ( ph /\ n e. W ) -> n e. ( ZZ>= ` ( M + K ) ) )
50 eluzsub 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ n e. ( ZZ>= ` ( M + K ) ) ) -> ( n - K ) e. ( ZZ>= ` M ) )
51 46 47 49 50 syl3anc 
 |-  ( ( ph /\ n e. W ) -> ( n - K ) e. ( ZZ>= ` M ) )
52 51 1 eleqtrrdi 
 |-  ( ( ph /\ n e. W ) -> ( n - K ) e. Z )
53 45 52 ffvelcdmd 
 |-  ( ( ph /\ n e. W ) -> ( F ` ( n - K ) ) e. ( CC ^m S ) )
54 6 53 fmpt3d 
 |-  ( ph -> H : W --> ( CC ^m S ) )
55 54 adantr 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> H : W --> ( CC ^m S ) )
56 6 ad2antrr 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ ( k e. W /\ z e. S ) ) -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
57 56 fveq1d 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ ( k e. W /\ z e. S ) ) -> ( H ` k ) = ( ( n e. W |-> ( F ` ( n - K ) ) ) ` k ) )
58 fvoveq1 
 |-  ( n = k -> ( F ` ( n - K ) ) = ( F ` ( k - K ) ) )
59 eqid 
 |-  ( n e. W |-> ( F ` ( n - K ) ) ) = ( n e. W |-> ( F ` ( n - K ) ) )
60 fvex 
 |-  ( F ` ( k - K ) ) e. _V
61 58 59 60 fvmpt 
 |-  ( k e. W -> ( ( n e. W |-> ( F ` ( n - K ) ) ) ` k ) = ( F ` ( k - K ) ) )
62 61 ad2antrl 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ ( k e. W /\ z e. S ) ) -> ( ( n e. W |-> ( F ` ( n - K ) ) ) ` k ) = ( F ` ( k - K ) ) )
63 57 62 eqtrd 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ ( k e. W /\ z e. S ) ) -> ( H ` k ) = ( F ` ( k - K ) ) )
64 63 fveq1d 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ ( k e. W /\ z e. S ) ) -> ( ( H ` k ) ` z ) = ( ( F ` ( k - K ) ) ` z ) )
65 eqidd 
 |-  ( ( ( ph /\ F ( ~~>u ` S ) G ) /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
66 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
67 66 adantl 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> G : S --> CC )
68 ulmscl 
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
69 68 adantl 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> S e. _V )
70 2 44 55 64 65 67 69 ulm2 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> ( H ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` ( k - K ) ) ` z ) - ( G ` z ) ) ) < x ) )
71 42 70 mpbird 
 |-  ( ( ph /\ F ( ~~>u ` S ) G ) -> H ( ~~>u ` S ) G )
72 71 ex 
 |-  ( ph -> ( F ( ~~>u ` S ) G -> H ( ~~>u ` S ) G ) )