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

Metamath Proof Explorer

Theorem itg1le

Description: If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion itg1le ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → 𝐹 ∈ dom ∫1 )
2 0ss ⊢ ∅ ⊆ ℝ
3 2 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ∅ ⊆ ℝ )
4 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
5 4 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( vol* ‘ ∅ ) = 0 )
6 simp2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → 𝐺 ∈ dom ∫1 )
7 simpl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 ∈ dom ∫1 )
8 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
9 ffn ⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
10 7 8 9 3syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 Fn ℝ )
11 simpr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 ∈ dom ∫1 )
12 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
13 ffn ⊢ ( 𝐺 : ℝ ⟶ ℝ → 𝐺 Fn ℝ )
14 11 12 13 3syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 Fn ℝ )
15 reex ⊢ ℝ ∈ V
16 15 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ℝ ∈ V )
17 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
18 eqidd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19 eqidd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
20 10 14 16 16 17 18 19 ofrval ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) ∧ 𝐹 ∘r ≤ 𝐺 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
21 20 3exp ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘r ≤ 𝐺 → ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) )
22 21 3impia ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
23 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ ∅ ) → 𝑥 ∈ ℝ )
24 22 23 impel ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) ∧ 𝑥 ∈ ( ℝ ∖ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
25 1 3 5 6 24 itg1lea ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )