Metamath Proof Explorer

Theorem evth2

Description: The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 
|- X = U. J
bndth.2 
|- K = ( topGen ` ran (,) )
bndth.3 
|- ( ph -> J e. Comp )
bndth.4 
|- ( ph -> F e. ( J Cn K ) )
evth.5 
|- ( ph -> X =/= (/) )
Assertion evth2 
|- ( ph -> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) )

Proof

Step Hyp Ref Expression
1 bndth.1 
 |-  X = U. J
2 bndth.2 
 |-  K = ( topGen ` ran (,) )
3 bndth.3 
 |-  ( ph -> J e. Comp )
4 bndth.4 
 |-  ( ph -> F e. ( J Cn K ) )
5 evth.5 
 |-  ( ph -> X =/= (/) )
6 cmptop 
 |-  ( J e. Comp -> J e. Top )
7 3 6 syl 
 |-  ( ph -> J e. Top )
8 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
9 7 8 sylib 
 |-  ( ph -> J e. ( TopOn ` X ) )
10 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
11 2 unieqi 
 |-  U. K = U. ( topGen ` ran (,) )
12 10 11 eqtr4i 
 |-  RR = U. K
13 1 12 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> RR )
14 4 13 syl 
 |-  ( ph -> F : X --> RR )
15 14 feqmptd 
 |-  ( ph -> F = ( z e. X |-> ( F ` z ) ) )
16 15 4 eqeltrrd 
 |-  ( ph -> ( z e. X |-> ( F ` z ) ) e. ( J Cn K ) )
17 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
18 2 17 eqeltri 
 |-  K e. ( TopOn ` RR )
19 18 a1i 
 |-  ( ph -> K e. ( TopOn ` RR ) )
20 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
21 20 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
22 21 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
23 0cnd 
 |-  ( ph -> 0 e. CC )
24 19 22 23 cnmptc 
 |-  ( ph -> ( y e. RR |-> 0 ) e. ( K Cn ( TopOpen ` CCfld ) ) )
25 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
26 2 25 eqtri 
 |-  K = ( ( TopOpen ` CCfld ) |`t RR )
27 ax-resscn 
 |-  RR C_ CC
28 27 a1i 
 |-  ( ph -> RR C_ CC )
29 22 cnmptid 
 |-  ( ph -> ( y e. CC |-> y ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
30 26 22 28 29 cnmpt1res 
 |-  ( ph -> ( y e. RR |-> y ) e. ( K Cn ( TopOpen ` CCfld ) ) )
31 20 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
32 31 a1i 
 |-  ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
33 19 24 30 32 cnmpt12f 
 |-  ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) )
34 df-neg 
 |-  -u y = ( 0 - y )
35 renegcl 
 |-  ( y e. RR -> -u y e. RR )
36 34 35 eqeltrrid 
 |-  ( y e. RR -> ( 0 - y ) e. RR )
37 36 adantl 
 |-  ( ( ph /\ y e. RR ) -> ( 0 - y ) e. RR )
38 37 fmpttd 
 |-  ( ph -> ( y e. RR |-> ( 0 - y ) ) : RR --> RR )
39 38 frnd 
 |-  ( ph -> ran ( y e. RR |-> ( 0 - y ) ) C_ RR )
40 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( y e. RR |-> ( 0 - y ) ) C_ RR /\ RR C_ CC ) -> ( ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) <-> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
41 22 39 28 40 syl3anc 
 |-  ( ph -> ( ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( TopOpen ` CCfld ) ) <-> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
42 33 41 mpbid 
 |-  ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
43 26 oveq2i 
 |-  ( K Cn K ) = ( K Cn ( ( TopOpen ` CCfld ) |`t RR ) )
44 42 43 eleqtrrdi 
 |-  ( ph -> ( y e. RR |-> ( 0 - y ) ) e. ( K Cn K ) )
45 negeq 
 |-  ( y = ( F ` z ) -> -u y = -u ( F ` z ) )
46 34 45 eqtr3id 
 |-  ( y = ( F ` z ) -> ( 0 - y ) = -u ( F ` z ) )
47 9 16 19 44 46 cnmpt11 
 |-  ( ph -> ( z e. X |-> -u ( F ` z ) ) e. ( J Cn K ) )
48 1 2 3 47 5 evth 
 |-  ( ph -> E. x e. X A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) )
49 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
50 49 negeqd 
 |-  ( z = y -> -u ( F ` z ) = -u ( F ` y ) )
51 eqid 
 |-  ( z e. X |-> -u ( F ` z ) ) = ( z e. X |-> -u ( F ` z ) )
52 negex 
 |-  -u ( F ` y ) e. _V
53 50 51 52 fvmpt 
 |-  ( y e. X -> ( ( z e. X |-> -u ( F ` z ) ) ` y ) = -u ( F ` y ) )
54 53 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( z e. X |-> -u ( F ` z ) ) ` y ) = -u ( F ` y ) )
55 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
56 55 negeqd 
 |-  ( z = x -> -u ( F ` z ) = -u ( F ` x ) )
57 negex 
 |-  -u ( F ` x ) e. _V
58 56 51 57 fvmpt 
 |-  ( x e. X -> ( ( z e. X |-> -u ( F ` z ) ) ` x ) = -u ( F ` x ) )
59 58 ad2antlr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( z e. X |-> -u ( F ` z ) ) ` x ) = -u ( F ` x ) )
60 54 59 breq12d 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> -u ( F ` y ) <_ -u ( F ` x ) ) )
61 14 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
62 61 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( F ` x ) e. RR )
63 14 ffvelcdmda 
 |-  ( ( ph /\ y e. X ) -> ( F ` y ) e. RR )
64 63 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( F ` y ) e. RR )
65 62 64 lenegd 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( F ` x ) <_ ( F ` y ) <-> -u ( F ` y ) <_ -u ( F ` x ) ) )
66 60 65 bitr4d 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> ( F ` x ) <_ ( F ` y ) ) )
67 66 ralbidva 
 |-  ( ( ph /\ x e. X ) -> ( A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> A. y e. X ( F ` x ) <_ ( F ` y ) ) )
68 67 rexbidva 
 |-  ( ph -> ( E. x e. X A. y e. X ( ( z e. X |-> -u ( F ` z ) ) ` y ) <_ ( ( z e. X |-> -u ( F ` z ) ) ` x ) <-> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) ) )
69 48 68 mpbid 
 |-  ( ph -> E. x e. X A. y e. X ( F ` x ) <_ ( F ` y ) )