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 20 tgioo2
 |-  ( 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 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
62 61 adantr
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( F ` x ) e. RR )
63 14 ffvelrnda
 |-  ( ( 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 ) )