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 ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) )