Metamath Proof Explorer

Theorem ulmval

Description: Express the predicate: The sequence of functions F converges uniformly to G on S . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 ulmrel 
 |-  Rel ( ~~>u ` S )
2 1 brrelex12i 
 |-  ( F ( ~~>u ` S ) G -> ( F e. _V /\ G e. _V ) )
3 2 a1i 
 |-  ( S e. V -> ( F ( ~~>u ` S ) G -> ( F e. _V /\ G e. _V ) ) )
4 3simpa 
 |-  ( ( 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 ) -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC ) )
5 fvex 
 |-  ( ZZ>= ` n ) e. _V
6 fex 
 |-  ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ ( ZZ>= ` n ) e. _V ) -> F e. _V )
7 5 6 mpan2 
 |-  ( F : ( ZZ>= ` n ) --> ( CC ^m S ) -> F e. _V )
8 7 a1i 
 |-  ( S e. V -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) -> F e. _V ) )
9 fex 
 |-  ( ( G : S --> CC /\ S e. V ) -> G e. _V )
10 9 expcom 
 |-  ( S e. V -> ( G : S --> CC -> G e. _V ) )
11 8 10 anim12d 
 |-  ( S e. V -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC ) -> ( F e. _V /\ G e. _V ) ) )
12 4 11 syl5 
 |-  ( S e. V -> ( ( 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 ) -> ( F e. _V /\ G e. _V ) ) )
13 12 rexlimdvw 
 |-  ( S e. V -> ( 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 ) -> ( F e. _V /\ G e. _V ) ) )
14 df-ulm 
 |-  ~~>u = ( s e. _V |-> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )
15 oveq2 
 |-  ( s = S -> ( CC ^m s ) = ( CC ^m S ) )
16 15 feq3d 
 |-  ( s = S -> ( f : ( ZZ>= ` n ) --> ( CC ^m s ) <-> f : ( ZZ>= ` n ) --> ( CC ^m S ) ) )
17 feq2 
 |-  ( s = S -> ( y : s --> CC <-> y : S --> CC ) )
18 raleq 
 |-  ( s = S -> ( A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) )
19 18 rexralbidv 
 |-  ( s = S -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) )
20 19 ralbidv 
 |-  ( s = S -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) )
21 16 17 20 3anbi123d 
 |-  ( s = S -> ( ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) <-> ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) )
22 21 rexbidv 
 |-  ( s = S -> ( E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) <-> E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) )
23 22 opabbidv 
 |-  ( s = S -> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } = { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )
24 elex 
 |-  ( S e. V -> S e. _V )
25 simpr1 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> f : ( ZZ>= ` n ) --> ( CC ^m S ) )
26 uzssz 
 |-  ( ZZ>= ` n ) C_ ZZ
27 ovex 
 |-  ( CC ^m S ) e. _V
28 zex 
 |-  ZZ e. _V
29 elpm2r 
 |-  ( ( ( ( CC ^m S ) e. _V /\ ZZ e. _V ) /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ ( ZZ>= ` n ) C_ ZZ ) ) -> f e. ( ( CC ^m S ) ^pm ZZ ) )
30 27 28 29 mpanl12 
 |-  ( ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ ( ZZ>= ` n ) C_ ZZ ) -> f e. ( ( CC ^m S ) ^pm ZZ ) )
31 25 26 30 sylancl 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> f e. ( ( CC ^m S ) ^pm ZZ ) )
32 simpr2 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> y : S --> CC )
33 cnex 
 |-  CC e. _V
34 simpl 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> S e. V )
35 elmapg 
 |-  ( ( CC e. _V /\ S e. V ) -> ( y e. ( CC ^m S ) <-> y : S --> CC ) )
36 33 34 35 sylancr 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> ( y e. ( CC ^m S ) <-> y : S --> CC ) )
37 32 36 mpbird 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> y e. ( CC ^m S ) )
38 31 37 jca 
 |-  ( ( S e. V /\ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) ) -> ( f e. ( ( CC ^m S ) ^pm ZZ ) /\ y e. ( CC ^m S ) ) )
39 38 ex 
 |-  ( S e. V -> ( ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) -> ( f e. ( ( CC ^m S ) ^pm ZZ ) /\ y e. ( CC ^m S ) ) ) )
40 39 rexlimdvw 
 |-  ( S e. V -> ( E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) -> ( f e. ( ( CC ^m S ) ^pm ZZ ) /\ y e. ( CC ^m S ) ) ) )
41 40 ssopab2dv 
 |-  ( S e. V -> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } C_ { <. f , y >. | ( f e. ( ( CC ^m S ) ^pm ZZ ) /\ y e. ( CC ^m S ) ) } )
42 df-xp 
 |-  ( ( ( CC ^m S ) ^pm ZZ ) X. ( CC ^m S ) ) = { <. f , y >. | ( f e. ( ( CC ^m S ) ^pm ZZ ) /\ y e. ( CC ^m S ) ) }
43 41 42 sseqtrrdi 
 |-  ( S e. V -> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } C_ ( ( ( CC ^m S ) ^pm ZZ ) X. ( CC ^m S ) ) )
44 ovex 
 |-  ( ( CC ^m S ) ^pm ZZ ) e. _V
45 44 27 xpex 
 |-  ( ( ( CC ^m S ) ^pm ZZ ) X. ( CC ^m S ) ) e. _V
46 45 ssex 
 |-  ( { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } C_ ( ( ( CC ^m S ) ^pm ZZ ) X. ( CC ^m S ) ) -> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } e. _V )
47 43 46 syl 
 |-  ( S e. V -> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } e. _V )
48 14 23 24 47 fvmptd3 
 |-  ( S e. V -> ( ~~>u ` S ) = { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )
49 48 breqd 
 |-  ( S e. V -> ( F ( ~~>u ` S ) G <-> F { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } G ) )
50 simpl 
 |-  ( ( f = F /\ y = G ) -> f = F )
51 50 feq1d 
 |-  ( ( f = F /\ y = G ) -> ( f : ( ZZ>= ` n ) --> ( CC ^m S ) <-> F : ( ZZ>= ` n ) --> ( CC ^m S ) ) )
52 simpr 
 |-  ( ( f = F /\ y = G ) -> y = G )
53 52 feq1d 
 |-  ( ( f = F /\ y = G ) -> ( y : S --> CC <-> G : S --> CC ) )
54 50 fveq1d 
 |-  ( ( f = F /\ y = G ) -> ( f ` k ) = ( F ` k ) )
55 54 fveq1d 
 |-  ( ( f = F /\ y = G ) -> ( ( f ` k ) ` z ) = ( ( F ` k ) ` z ) )
56 52 fveq1d 
 |-  ( ( f = F /\ y = G ) -> ( y ` z ) = ( G ` z ) )
57 55 56 oveq12d 
 |-  ( ( f = F /\ y = G ) -> ( ( ( f ` k ) ` z ) - ( y ` z ) ) = ( ( ( F ` k ) ` z ) - ( G ` z ) ) )
58 57 fveq2d 
 |-  ( ( f = F /\ y = G ) -> ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) )
59 58 breq1d 
 |-  ( ( f = F /\ y = G ) -> ( ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) )
60 59 ralbidv 
 |-  ( ( f = F /\ y = G ) -> ( A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) )
61 60 rexralbidv 
 |-  ( ( f = F /\ y = G ) -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) )
62 61 ralbidv 
 |-  ( ( f = F /\ y = G ) -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x <-> 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 ) )
63 51 53 62 3anbi123d 
 |-  ( ( f = F /\ y = G ) -> ( ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) <-> ( 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 ) ) )
64 63 rexbidv 
 |-  ( ( f = F /\ y = G ) -> ( E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) <-> 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 ) ) )
65 eqid 
 |-  { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } = { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) }
66 64 65 brabga 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m S ) /\ y : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } 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 ) ) )
67 49 66 sylan9bb 
 |-  ( ( S e. V /\ ( F e. _V /\ G 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 ) ) )
68 67 ex 
 |-  ( S e. V -> ( ( F e. _V /\ G 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 ) ) ) )
69 3 13 68 pm5.21ndd 
 |-  ( 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 ) ) )