Metamath Proof Explorer


Theorem stoweidlem29

Description: When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses stoweidlem29.1 𝑡 𝐹
stoweidlem29.2 𝑡 𝜑
stoweidlem29.3 𝑇 = 𝐽
stoweidlem29.4 𝐾 = ( topGen ‘ ran (,) )
stoweidlem29.5 ( 𝜑𝐽 ∈ Comp )
stoweidlem29.6 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
stoweidlem29.7 ( 𝜑𝑇 ≠ ∅ )
Assertion stoweidlem29 ( 𝜑 → ( inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem29.1 𝑡 𝐹
2 stoweidlem29.2 𝑡 𝜑
3 stoweidlem29.3 𝑇 = 𝐽
4 stoweidlem29.4 𝐾 = ( topGen ‘ ran (,) )
5 stoweidlem29.5 ( 𝜑𝐽 ∈ Comp )
6 stoweidlem29.6 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7 stoweidlem29.7 ( 𝜑𝑇 ≠ ∅ )
8 eqid ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
9 4 3 8 6 fcnre ( 𝜑𝐹 : 𝑇 ⟶ ℝ )
10 df-f ( 𝐹 : 𝑇 ⟶ ℝ ↔ ( 𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ ) )
11 9 10 sylib ( 𝜑 → ( 𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ ) )
12 11 simprd ( 𝜑 → ran 𝐹 ⊆ ℝ )
13 11 simpld ( 𝜑𝐹 Fn 𝑇 )
14 fnfun ( 𝐹 Fn 𝑇 → Fun 𝐹 )
15 13 14 syl ( 𝜑 → Fun 𝐹 )
16 15 adantr ( ( 𝜑𝑠𝑇 ) → Fun 𝐹 )
17 9 fdmd ( 𝜑 → dom 𝐹 = 𝑇 )
18 17 eqcomd ( 𝜑𝑇 = dom 𝐹 )
19 18 eleq2d ( 𝜑 → ( 𝑠𝑇𝑠 ∈ dom 𝐹 ) )
20 19 biimpa ( ( 𝜑𝑠𝑇 ) → 𝑠 ∈ dom 𝐹 )
21 fvelrn ( ( Fun 𝐹𝑠 ∈ dom 𝐹 ) → ( 𝐹𝑠 ) ∈ ran 𝐹 )
22 16 20 21 syl2anc ( ( 𝜑𝑠𝑇 ) → ( 𝐹𝑠 ) ∈ ran 𝐹 )
23 nfcv 𝑡 𝑠
24 1 23 nffv 𝑡 ( 𝐹𝑠 )
25 24 nfeq2 𝑡 𝑥 = ( 𝐹𝑠 )
26 breq1 ( 𝑥 = ( 𝐹𝑠 ) → ( 𝑥 ≤ ( 𝐹𝑡 ) ↔ ( 𝐹𝑠 ) ≤ ( 𝐹𝑡 ) ) )
27 25 26 ralbid ( 𝑥 = ( 𝐹𝑠 ) → ( ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ↔ ∀ 𝑡𝑇 ( 𝐹𝑠 ) ≤ ( 𝐹𝑡 ) ) )
28 27 rspcev ( ( ( 𝐹𝑠 ) ∈ ran 𝐹 ∧ ∀ 𝑡𝑇 ( 𝐹𝑠 ) ≤ ( 𝐹𝑡 ) ) → ∃ 𝑥 ∈ ran 𝐹𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) )
29 22 28 sylan ( ( ( 𝜑𝑠𝑇 ) ∧ ∀ 𝑡𝑇 ( 𝐹𝑠 ) ≤ ( 𝐹𝑡 ) ) → ∃ 𝑥 ∈ ran 𝐹𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) )
30 nfcv 𝑠 𝐹
31 nfcv 𝑠 𝑇
32 nfcv 𝑡 𝑇
33 30 1 31 32 3 4 5 6 7 evth2f ( 𝜑 → ∃ 𝑠𝑇𝑡𝑇 ( 𝐹𝑠 ) ≤ ( 𝐹𝑡 ) )
34 29 33 r19.29a ( 𝜑 → ∃ 𝑥 ∈ ran 𝐹𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) )
35 nfv 𝑦 ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) )
36 simpr ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ran 𝐹 )
37 13 ad2antrr ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐹 Fn 𝑇 )
38 nfcv 𝑡 𝑦
39 32 38 1 fvelrnbf ( 𝐹 Fn 𝑇 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑡𝑇 ( 𝐹𝑡 ) = 𝑦 ) )
40 37 39 syl ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑡𝑇 ( 𝐹𝑡 ) = 𝑦 ) )
41 36 40 mpbid ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑡𝑇 ( 𝐹𝑡 ) = 𝑦 )
42 nfra1 𝑡𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 )
43 2 42 nfan 𝑡 ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) )
44 1 nfrn 𝑡 ran 𝐹
45 44 nfcri 𝑡 𝑦 ∈ ran 𝐹
46 43 45 nfan 𝑡 ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 )
47 nfv 𝑡 𝑥𝑦
48 rspa ( ( ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ∧ 𝑡𝑇 ) → 𝑥 ≤ ( 𝐹𝑡 ) )
49 breq2 ( ( 𝐹𝑡 ) = 𝑦 → ( 𝑥 ≤ ( 𝐹𝑡 ) ↔ 𝑥𝑦 ) )
50 48 49 syl5ibcom ( ( ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ∧ 𝑡𝑇 ) → ( ( 𝐹𝑡 ) = 𝑦𝑥𝑦 ) )
51 50 ex ( ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) → ( 𝑡𝑇 → ( ( 𝐹𝑡 ) = 𝑦𝑥𝑦 ) ) )
52 51 ad2antlr ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑡𝑇 → ( ( 𝐹𝑡 ) = 𝑦𝑥𝑦 ) ) )
53 46 47 52 rexlimd ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ∃ 𝑡𝑇 ( 𝐹𝑡 ) = 𝑦𝑥𝑦 ) )
54 41 53 mpd ( ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑥𝑦 )
55 54 ex ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) → ( 𝑦 ∈ ran 𝐹𝑥𝑦 ) )
56 35 55 ralrimi ( ( 𝜑 ∧ ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑥𝑦 )
57 56 ex ( 𝜑 → ( ∀ 𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) → ∀ 𝑦 ∈ ran 𝐹 𝑥𝑦 ) )
58 57 reximdv ( 𝜑 → ( ∃ 𝑥 ∈ ran 𝐹𝑡𝑇 𝑥 ≤ ( 𝐹𝑡 ) → ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 𝑥𝑦 ) )
59 34 58 mpd ( 𝜑 → ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 𝑥𝑦 )
60 lbinfcl ( ( ran 𝐹 ⊆ ℝ ∧ ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 𝑥𝑦 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
61 12 59 60 syl2anc ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
62 12 61 sseldd ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
63 12 adantr ( ( 𝜑𝑡𝑇 ) → ran 𝐹 ⊆ ℝ )
64 59 adantr ( ( 𝜑𝑡𝑇 ) → ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 𝑥𝑦 )
65 dffn3 ( 𝐹 Fn 𝑇𝐹 : 𝑇 ⟶ ran 𝐹 )
66 13 65 sylib ( 𝜑𝐹 : 𝑇 ⟶ ran 𝐹 )
67 66 ffvelrnda ( ( 𝜑𝑡𝑇 ) → ( 𝐹𝑡 ) ∈ ran 𝐹 )
68 lbinfle ( ( ran 𝐹 ⊆ ℝ ∧ ∃ 𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐹 𝑥𝑦 ∧ ( 𝐹𝑡 ) ∈ ran 𝐹 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) )
69 63 64 67 68 syl3anc ( ( 𝜑𝑡𝑇 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) )
70 69 ex ( 𝜑 → ( 𝑡𝑇 → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) ) )
71 2 70 ralrimi ( 𝜑 → ∀ 𝑡𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) )
72 61 62 71 3jca ( 𝜑 → ( inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹𝑡 ) ) )