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	biimtrrid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 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 )