This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 tgioo4 ⊢ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
63 14 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
64 63 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
65 62 64 lenegd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑥 ) ) )
66 60 65 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
67 66 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
68 67 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑦 ) ≤ ( ( 𝑧 ∈ 𝑋 ↦ - ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
69 48 68 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )