Metamath Proof Explorer

Theorem itg10a

Description: The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg10a.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
itg10a.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
itg10a.3 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
itg10a.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
Assertion itg10a ( 𝜑 → ( ∫1 ‘ 𝐹 ) = 0 )

Proof

Step Hyp Ref Expression
1 itg10a.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 itg10a.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 itg10a.3 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
4 itg10a.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
5 itg1val ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
6 1 5 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) )
7 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
8 1 7 syl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
9 8 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐹 Fn ℝ )
11 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
13 eldifsni ⊢ ( 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑘 ≠ 0 )
14 13 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 𝑘 ≠ 0 )
15 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 𝑥 ∈ ℝ )
16 eldif ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) )
17 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑘 )
18 4 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
19 17 18 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 𝑘 = 0 )
20 19 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑘 = 0 ) )
21 16 20 syl5bir ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) → 𝑘 = 0 ) )
22 15 21 mpand ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( ¬ 𝑥 ∈ 𝐴 → 𝑘 = 0 ) )
23 22 necon1ad ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → ( 𝑘 ≠ 0 → 𝑥 ∈ 𝐴 ) )
24 14 23 mpd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) → 𝑥 ∈ 𝐴 )
25 24 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) → 𝑥 ∈ 𝐴 ) )
26 12 25 sylbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) → 𝑥 ∈ 𝐴 ) )
27 26 ssrdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ 𝐴 )
28 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐴 ⊆ ℝ )
29 27 28 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ )
30 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol* ‘ 𝐴 ) = 0 )
31 ovolssnul ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
32 27 28 30 31 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
33 nulmbl ⊢ ( ( ( ◡ 𝐹 “ { 𝑘 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 ) → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
34 29 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol )
35 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑘 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) )
37 36 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) = 0 )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = ( 𝑘 · 0 ) )
39 8 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
40 39 ssdifssd ⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
41 40 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑘 ∈ ℂ )
43 42 mul01d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑘 · 0 ) = 0 )
44 38 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = 0 )
45 44 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) 0 )
46 i1frn ⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
47 1 46 syl ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
48 difss ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹
49 ssfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
50 47 48 49 sylancl ⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ∈ Fin )
51 50 olcd ⊢ ( 𝜑 → ( ( ran 𝐹 ∖ { 0 } ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) )
52 sumz ⊢ ( ( ( ran 𝐹 ∖ { 0 } ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( ran 𝐹 ∖ { 0 } ) ∈ Fin ) → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) 0 = 0 )
53 51 52 syl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) 0 = 0 )
54 45 53 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑘 · ( vol ‘ ( ◡ 𝐹 “ { 𝑘 } ) ) ) = 0 )
55 6 54 eqtrd ⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = 0 )