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 ) )