Metamath Proof Explorer

Theorem ofsubge0

Description: Function analogue of subge0 . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion ofsubge0 ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( ( 𝐴 × { 0 } ) ∘r ≤ ( 𝐹 ∘f − 𝐺 ) ↔ 𝐺 ∘r ≤ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
2 1 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
3 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → 𝐺 : 𝐴 ⟶ ℝ )
4 3 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
5 2 4 subge0d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
6 5 ralbidva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 0 ≤ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
7 0cn ⊢ 0 ∈ ℂ
8 fnconstg ⊢ ( 0 ∈ ℂ → ( 𝐴 × { 0 } ) Fn 𝐴 )
9 7 8 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( 𝐴 × { 0 } ) Fn 𝐴 )
10 1 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → 𝐹 Fn 𝐴 )
11 3 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → 𝐺 Fn 𝐴 )
12 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → 𝐴 ∈ 𝑉 )
13 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
14 10 11 12 12 13 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( 𝐹 ∘f − 𝐺 ) Fn 𝐴 )
15 c0ex ⊢ 0 ∈ V
16 15 fvconst2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
18 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
20 10 11 12 12 13 18 19 ofval ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f − 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
21 9 14 12 12 13 17 20 ofrfval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( ( 𝐴 × { 0 } ) ∘r ≤ ( 𝐹 ∘f − 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐴 0 ≤ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
22 11 10 12 12 13 19 18 ofrfval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( 𝐺 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
23 6 21 22 3bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( ( 𝐴 × { 0 } ) ∘r ≤ ( 𝐹 ∘f − 𝐺 ) ↔ 𝐺 ∘r ≤ 𝐹 ) )