Metamath Proof Explorer

Theorem extoimad

Description: If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses extoimad.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
extoimad.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝐶 )
Assertion extoimad ( 𝜑 → ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 𝐶 )

Proof

Step Hyp Ref Expression
1 extoimad.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 extoimad.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝐶 )
3 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
4 3 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
5 4 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
6 imaco ⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) )
7 6 a1i ⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) ) )
8 7 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) ↔ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) ) )
9 absf ⊢ abs : ℂ ⟶ ℝ
10 9 a1i ⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
11 ax-resscn ⊢ ℝ ⊆ ℂ
12 11 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
13 10 12 fssresd ⊢ ( 𝜑 → ( abs ↾ ℝ ) : ℝ ⟶ ℝ )
14 1 13 fco2d ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) : ℝ ⟶ ℝ )
15 14 ffnd ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) Fn ℝ )
16 ssidd ⊢ ( 𝜑 → ℝ ⊆ ℝ )
17 15 16 fvelimabd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) ↔ ∃ 𝑦 ∈ ℝ ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = 𝑥 ) )
18 eqcom ⊢ ( ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) )
19 18 a1i ⊢ ( 𝜑 → ( ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = 𝑥 ↔ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
20 19 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = 𝑥 ↔ ∃ 𝑦 ∈ ℝ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
21 17 20 bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) ↔ ∃ 𝑦 ∈ ℝ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
24 22 23 fvco3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
25 24 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) )
26 25 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ↔ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
27 26 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℝ 𝑥 = ( ( abs ∘ 𝐹 ) ‘ 𝑦 ) ) )
28 21 27 bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) ↔ ∃ 𝑦 ∈ ℝ 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
29 8 28 bitr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) ↔ ∃ 𝑦 ∈ ℝ 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
31 30 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ≤ 𝐶 ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝐶 ) )
32 5 29 31 ralxfr2d ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 𝐶 ↔ ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝐶 ) )
33 2 32 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 𝐶 )