Metamath Proof Explorer

Theorem itg1ge0

Description: Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014)

Ref Expression
Assertion itg1ge0 ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 0 ≤ ( ∫1 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 i1frn ⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
2 difss ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
3 ssfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
4 1 2 3 sylancl ⊢ ( 𝐹 ∈ dom ∫1 → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
5 4 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
6 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
7 6 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ℝ )
8 7 frnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ran 𝐹 ⊆ ℝ )
9 8 ssdifssd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
10 9 sselda ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ ℝ )
11 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
12 11 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
13 10 12 remulcld ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℝ )
14 eldifi ⊢ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑥 ∈ ran 𝐹 )
15 0cn ⊢ 0 ∈ ℂ
16 fnconstg ⊢ ( 0 ∈ ℂ → ( ℂ × { 0 } ) Fn ℂ )
17 15 16 ax-mp ⊢ ( ℂ × { 0 } ) Fn ℂ
18 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
19 18 fneq1i ⊢ ( 0𝑝 Fn ℂ ↔ ( ℂ × { 0 } ) Fn ℂ )
20 17 19 mpbir ⊢ 0𝑝 Fn ℂ
21 20 a1i ⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 Fn ℂ )
22 6 ffnd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 Fn ℝ )
23 cnex ⊢ ℂ ∈ V
24 23 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℂ ∈ V )
25 reex ⊢ ℝ ∈ V
26 25 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 sseqin2 ⊢ ( ℝ ⊆ ℂ ↔ ( ℂ ∩ ℝ ) = ℝ )
29 27 28 mpbi ⊢ ( ℂ ∩ ℝ ) = ℝ
30 0pval ⊢ ( 𝑦 ∈ ℂ → ( 0𝑝 ‘ 𝑦 ) = 0 )
31 30 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑦 ∈ ℂ ) → ( 0𝑝 ‘ 𝑦 ) = 0 )
32 eqidd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
33 21 22 24 26 29 31 32 ofrfval ⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
34 33 biimpa ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) )
35 22 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 Fn ℝ )
36 breq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 0 ≤ 𝑥 ↔ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
37 36 ralrn ⊢ ( 𝐹 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐹 0 ≤ 𝑥 ↔ ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
38 35 37 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∀ 𝑥 ∈ ran 𝐹 0 ≤ 𝑥 ↔ ∀ 𝑦 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
39 34 38 mpbird ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ ran 𝐹 0 ≤ 𝑥 )
40 39 r19.21bi ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ran 𝐹 ) → 0 ≤ 𝑥 )
41 14 40 sylan2 ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 0 ≤ 𝑥 )
42 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
43 42 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
44 mblss ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ )
45 ovolge0 ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
46 44 45 syl ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → 0 ≤ ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
47 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
48 46 47 breqtrrd ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → 0 ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
49 43 48 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 0 ≤ ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
50 10 12 41 49 mulge0d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 0 ≤ ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
51 5 13 50 fsumge0 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 0 ≤ Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
52 itg1val ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
53 52 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
54 51 53 breqtrrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 0 ≤ ( ∫1 ‘ 𝐹 ) )