Metamath Proof Explorer

Theorem ulm2

Description: Simplify ulmval when F and G are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses ulm2.z 
|- Z = ( ZZ>= ` M )
ulm2.m 
|- ( ph -> M e. ZZ )
ulm2.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
ulm2.b 
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = B )
ulm2.a 
|- ( ( ph /\ z e. S ) -> ( G ` z ) = A )
ulm2.g 
|- ( ph -> G : S --> CC )
ulm2.s 
|- ( ph -> S e. V )
Assertion ulm2 
|- ( ph -> ( F ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )

Proof

Step Hyp Ref Expression
1 ulm2.z 
 |-  Z = ( ZZ>= ` M )
2 ulm2.m 
 |-  ( ph -> M e. ZZ )
3 ulm2.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
4 ulm2.b 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = B )
5 ulm2.a 
 |-  ( ( ph /\ z e. S ) -> ( G ` z ) = A )
6 ulm2.g 
 |-  ( ph -> G : S --> CC )
7 ulm2.s 
 |-  ( ph -> S e. V )
8 ulmval 
 |-  ( S e. V -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
9 7 8 syl 
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
10 3anan12 
 |-  ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
11 3 fdmd 
 |-  ( ph -> dom F = Z )
12 fdm 
 |-  ( F : ( ZZ>= ` n ) --> ( CC ^m S ) -> dom F = ( ZZ>= ` n ) )
13 11 12 sylan9req 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> Z = ( ZZ>= ` n ) )
14 1 13 eqtr3id 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( ZZ>= ` M ) = ( ZZ>= ` n ) )
15 2 adantr 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> M e. ZZ )
16 uz11 
 |-  ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` n ) <-> M = n ) )
17 15 16 syl 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( ( ZZ>= ` M ) = ( ZZ>= ` n ) <-> M = n ) )
18 14 17 mpbid 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> M = n )
19 18 eqcomd 
 |-  ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> n = M )
20 fveq2 
 |-  ( n = M -> ( ZZ>= ` n ) = ( ZZ>= ` M ) )
21 20 1 eqtr4di 
 |-  ( n = M -> ( ZZ>= ` n ) = Z )
22 21 feq2d 
 |-  ( n = M -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) <-> F : Z --> ( CC ^m S ) ) )
23 22 biimparc 
 |-  ( ( F : Z --> ( CC ^m S ) /\ n = M ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) )
24 3 23 sylan 
 |-  ( ( ph /\ n = M ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) )
25 19 24 impbida 
 |-  ( ph -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) <-> n = M ) )
26 25 anbi1d 
 |-  ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) )
27 6 biantrurd 
 |-  ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) )
28 simp-4l 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ph )
29 simpr 
 |-  ( ( ph /\ n = M ) -> n = M )
30 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
31 2 30 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
32 31 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
33 32 adantr 
 |-  ( ( ph /\ n = M ) -> M e. Z )
34 29 33 eqeltrd 
 |-  ( ( ph /\ n = M ) -> n e. Z )
35 1 uztrn2 
 |-  ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
36 34 35 sylan 
 |-  ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
37 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
38 36 37 sylan 
 |-  ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
39 38 adantr 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> k e. Z )
40 simpr 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> z e. S )
41 28 39 40 4 syl12anc 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) = B )
42 28 5 sylancom 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( G ` z ) = A )
43 41 42 oveq12d 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( ( F ` k ) ` z ) - ( G ` z ) ) = ( B - A ) )
44 43 fveq2d 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( B - A ) ) )
45 44 breq1d 
 |-  ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
46 45 ralbidva 
 |-  ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. z e. S ( abs ` ( B - A ) ) < x ) )
47 46 ralbidva 
 |-  ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
48 47 rexbidva 
 |-  ( ( ph /\ n = M ) -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
49 48 ralbidv 
 |-  ( ( ph /\ n = M ) -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
50 49 pm5.32da 
 |-  ( ph -> ( ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) )
51 26 27 50 3bitr3d 
 |-  ( ph -> ( ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) )
52 10 51 syl5bb 
 |-  ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) )
53 52 rexbidv 
 |-  ( ph -> ( E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) )
54 21 rexeqdv 
 |-  ( n = M -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
55 54 ralbidv 
 |-  ( n = M -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
56 55 ceqsrexv 
 |-  ( M e. ZZ -> ( E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
57 2 56 syl 
 |-  ( ph -> ( E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )
58 9 53 57 3bitrd 
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) )