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 𝑋 = 𝐽
bndth.2 𝐾 = ( topGen ‘ ran (,) )
bndth.3 ( 𝜑𝐽 ∈ Comp )
bndth.4 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
evth.5 ( 𝜑𝑋 ≠ ∅ )
Assertion evth2 ( 𝜑 → ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )

Proof

Step Hyp Ref Expression
1 bndth.1 𝑋 = 𝐽
2 bndth.2 𝐾 = ( topGen ‘ ran (,) )
3 bndth.3 ( 𝜑𝐽 ∈ Comp )
4 bndth.4 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 evth.5 ( 𝜑𝑋 ≠ ∅ )
6 cmptop ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
7 3 6 syl ( 𝜑𝐽 ∈ Top )
8 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 7 8 sylib ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 uniretop ℝ = ( topGen ‘ ran (,) )
11 2 unieqi 𝐾 = ( topGen ‘ ran (,) )
12 10 11 eqtr4i ℝ = 𝐾
13 1 12 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ℝ )
14 4 13 syl ( 𝜑𝐹 : 𝑋 ⟶ ℝ )
15 14 feqmptd ( 𝜑𝐹 = ( 𝑧𝑋 ↦ ( 𝐹𝑧 ) ) )
16 15 4 eqeltrrd ( 𝜑 → ( 𝑧𝑋 ↦ ( 𝐹𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
17 retopon ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
18 2 17 eqeltri 𝐾 ∈ ( TopOn ‘ ℝ )
19 18 a1i ( 𝜑𝐾 ∈ ( TopOn ‘ ℝ ) )
20 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21 20 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
22 21 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
23 0cnd ( 𝜑 → 0 ∈ ℂ )
24 19 22 23 cnmptc ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 0 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
25 20 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
26 2 25 eqtri 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27 ax-resscn ℝ ⊆ ℂ
28 27 a1i ( 𝜑 → ℝ ⊆ ℂ )
29 22 cnmptid ( 𝜑 → ( 𝑦 ∈ ℂ ↦ 𝑦 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
30 26 22 28 29 cnmpt1res ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 𝑦 ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
31 20 subcn − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
32 31 a1i ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
33 19 24 30 32 cnmpt12f ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) )
34 df-neg - 𝑦 = ( 0 − 𝑦 )
35 renegcl ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
36 34 35 eqeltrrid ( 𝑦 ∈ ℝ → ( 0 − 𝑦 ) ∈ ℝ )
37 36 adantl ( ( 𝜑𝑦 ∈ ℝ ) → ( 0 − 𝑦 ) ∈ ℝ )
38 37 fmpttd ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) : ℝ ⟶ ℝ )
39 38 frnd ( 𝜑 → ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ )
40 cnrest2 ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
41 22 39 28 40 syl3anc ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
42 33 41 mpbid ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
43 26 oveq2i ( 𝐾 Cn 𝐾 ) = ( 𝐾 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
44 42 43 eleqtrrdi ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 0 − 𝑦 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
45 negeq ( 𝑦 = ( 𝐹𝑧 ) → - 𝑦 = - ( 𝐹𝑧 ) )
46 34 45 eqtr3id ( 𝑦 = ( 𝐹𝑧 ) → ( 0 − 𝑦 ) = - ( 𝐹𝑧 ) )
47 9 16 19 44 46 cnmpt11 ( 𝜑 → ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
48 1 2 3 47 5 evth ( 𝜑 → ∃ 𝑥𝑋𝑦𝑋 ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) )
49 fveq2 ( 𝑧 = 𝑦 → ( 𝐹𝑧 ) = ( 𝐹𝑦 ) )
50 49 negeqd ( 𝑧 = 𝑦 → - ( 𝐹𝑧 ) = - ( 𝐹𝑦 ) )
51 eqid ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) = ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) )
52 negex - ( 𝐹𝑦 ) ∈ V
53 50 51 52 fvmpt ( 𝑦𝑋 → ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹𝑦 ) )
54 53 adantl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) = - ( 𝐹𝑦 ) )
55 fveq2 ( 𝑧 = 𝑥 → ( 𝐹𝑧 ) = ( 𝐹𝑥 ) )
56 55 negeqd ( 𝑧 = 𝑥 → - ( 𝐹𝑧 ) = - ( 𝐹𝑥 ) )
57 negex - ( 𝐹𝑥 ) ∈ V
58 56 51 57 fvmpt ( 𝑥𝑋 → ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹𝑥 ) )
59 58 ad2antlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) = - ( 𝐹𝑥 ) )
60 54 59 breq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) ↔ - ( 𝐹𝑦 ) ≤ - ( 𝐹𝑥 ) ) )
61 14 ffvelrnda ( ( 𝜑𝑥𝑋 ) → ( 𝐹𝑥 ) ∈ ℝ )
62 61 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( 𝐹𝑥 ) ∈ ℝ )
63 14 ffvelrnda ( ( 𝜑𝑦𝑋 ) → ( 𝐹𝑦 ) ∈ ℝ )
64 63 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( 𝐹𝑦 ) ∈ ℝ )
65 62 64 lenegd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ↔ - ( 𝐹𝑦 ) ≤ - ( 𝐹𝑥 ) ) )
66 60 65 bitr4d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) ↔ ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
67 66 ralbidva ( ( 𝜑𝑥𝑋 ) → ( ∀ 𝑦𝑋 ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) ↔ ∀ 𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
68 67 rexbidva ( 𝜑 → ( ∃ 𝑥𝑋𝑦𝑋 ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧𝑋 ↦ - ( 𝐹𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) ) )
69 48 68 mpbid ( 𝜑 → ∃ 𝑥𝑋𝑦𝑋 ( 𝐹𝑥 ) ≤ ( 𝐹𝑦 ) )