Metamath Proof Explorer

Theorem itg1val2

Description: The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion itg1val2 ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ 𝐴 ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )

Proof

Step Hyp Ref Expression
1 itg1val ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
2 1 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
3 simpr2 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 )
4 3 sselda ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ 𝐴 )
5 simpr3 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → 𝐴 ⊆ ( ℝ ∖ { 0 } ) )
6 5 sselda ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( ℝ ∖ { 0 } ) )
7 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) → 𝑥 ∈ ℝ )
8 6 7 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
9 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
10 9 adantlr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
11 6 10 syldan ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
12 8 11 remulcld ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℝ )
13 12 recnd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℂ )
14 4 13 syldan ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ ℂ )
15 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
16 15 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝐹 : ℝ ⟶ ℝ )
17 ffrn ⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 : ℝ ⟶ ran 𝐹 )
18 16 17 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝐹 : ℝ ⟶ ran 𝐹 )
19 eldifn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) → ¬ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
20 19 adantl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ¬ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
21 eldif ⊢ ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ( 𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ { 0 } ) )
22 simplr3 ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝐴 ⊆ ( ℝ ∖ { 0 } ) )
23 22 ssdifssd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ⊆ ( ℝ ∖ { 0 } ) )
24 simpr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) )
25 23 24 sseldd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝑥 ∈ ( ℝ ∖ { 0 } ) )
26 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) → ¬ 𝑥 ∈ { 0 } )
27 25 26 syl ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ¬ 𝑥 ∈ { 0 } )
28 27 biantrud ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝑥 ∈ ran 𝐹 ↔ ( 𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ { 0 } ) ) )
29 21 28 bitr4id ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ 𝑥 ∈ ran 𝐹 ) )
30 20 29 mtbid ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ¬ 𝑥 ∈ ran 𝐹 )
31 disjsn ⊢ ( ( ran 𝐹 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹 )
32 30 31 sylibr ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( ran 𝐹 ∩ { 𝑥 } ) = ∅ )
33 fimacnvdisj ⊢ ( ( 𝐹 : ℝ ⟶ ran 𝐹 ∧ ( ran 𝐹 ∩ { 𝑥 } ) = ∅ ) → ( ◡ 𝐹 “ { 𝑥 } ) = ∅ )
34 18 32 33 syl2anc ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( ◡ 𝐹 “ { 𝑥 } ) = ∅ )
35 34 fveq2d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( vol ‘ ∅ ) )
36 0mbl ⊢ ∅ ∈ dom vol
37 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
38 36 37 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
39 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
40 38 39 eqtri ⊢ ( vol ‘ ∅ ) = 0
41 35 40 eqtrdi ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = 0 )
42 41 oveq2d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) = ( 𝑥 · 0 ) )
43 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) → 𝑥 ∈ 𝐴 )
44 43 8 sylan2 ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝑥 ∈ ℝ )
45 44 recnd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → 𝑥 ∈ ℂ )
46 45 mul01d ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝑥 · 0 ) = 0 )
47 42 46 eqtrd ⊢ ( ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) = 0 )
48 simpr1 ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → 𝐴 ∈ Fin )
49 3 14 47 48 fsumss ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) = Σ 𝑥 ∈ 𝐴 ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )
50 2 49 eqtrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝐴 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ 𝐴 ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )