Metamath Proof Explorer

Theorem itg11

Description: The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis i1f1.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
Assertion itg11 ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
2 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
3 0mbl ⊢ ∅ ∈ dom vol
4 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
5 3 4 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
6 itg10 ⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = 0
7 2 5 6 3eqtr4ri ⊢ ( ∫1 ‘ ( ℝ × { 0 } ) ) = ( vol ‘ ∅ )
8 noel ⊢ ¬ 𝑥 ∈ ∅
9 eleq2 ⊢ ( 𝐴 = ∅ → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ∅ ) )
10 8 9 mtbiri ⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 )
11 10 iffalsed ⊢ ( 𝐴 = ∅ → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 0 )
12 11 mpteq2dv ⊢ ( 𝐴 = ∅ → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
13 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
14 12 1 13 3eqtr4g ⊢ ( 𝐴 = ∅ → 𝐹 = ( ℝ × { 0 } ) )
15 14 fveq2d ⊢ ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( ∫1 ‘ ( ℝ × { 0 } ) ) )
16 fveq2 ⊢ ( 𝐴 = ∅ → ( vol ‘ 𝐴 ) = ( vol ‘ ∅ ) )
17 7 15 16 3eqtr4a ⊢ ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) )
18 17 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 = ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) )
19 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
20 1 i1f1 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 )
21 20 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝐹 ∈ dom ∫1 )
22 itg1val ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ∫1 ‘ 𝐹 ) = Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) )
24 1 i1f1lem ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) )
25 24 simpli ⊢ 𝐹 : ℝ ⟶ { 0 , 1 }
26 frn ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → ran 𝐹 ⊆ { 0 , 1 } )
27 25 26 ax-mp ⊢ ran 𝐹 ⊆ { 0 , 1 }
28 ssdif ⊢ ( ran 𝐹 ⊆ { 0 , 1 } → ( ran 𝐹 ∖ { 0 } ) ⊆ ( { 0 , 1 } ∖ { 0 } ) )
29 27 28 ax-mp ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ( { 0 , 1 } ∖ { 0 } )
30 difprsnss ⊢ ( { 0 , 1 } ∖ { 0 } ) ⊆ { 1 }
31 29 30 sstri ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 }
32 31 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 } )
33 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
34 33 adantr ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐴 ⊆ ℝ )
35 34 sselda ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
36 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
37 36 ifbid ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) )
38 1ex ⊢ 1 ∈ V
39 c0ex ⊢ 0 ∈ V
40 38 39 ifex ⊢ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ∈ V
41 37 1 40 fvmpt ⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) )
42 35 41 syl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) )
43 iftrue ⊢ ( 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 )
44 43 adantl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 )
45 42 44 eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = 1 )
46 ffn ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → 𝐹 Fn ℝ )
47 25 46 ax-mp ⊢ 𝐹 Fn ℝ
48 fnfvelrn ⊢ ( ( 𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
49 47 35 48 sylancr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
50 45 49 eqeltrrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 1 ∈ ran 𝐹 )
51 ax-1ne0 ⊢ 1 ≠ 0
52 eldifsn ⊢ ( 1 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ( 1 ∈ ran 𝐹 ∧ 1 ≠ 0 ) )
53 50 51 52 sylanblrc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 1 ∈ ( ran 𝐹 ∖ { 0 } ) )
54 53 snssd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → { 1 } ⊆ ( ran 𝐹 ∖ { 0 } ) )
55 32 54 eqssd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ran 𝐹 ∖ { 0 } ) = { 1 } )
56 55 sumeq1d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) )
57 1re ⊢ 1 ∈ ℝ
58 24 simpri ⊢ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 )
59 58 ad2antrr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 1 } ) = 𝐴 )
60 59 fveq2d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) = ( vol ‘ 𝐴 ) )
61 60 oveq2d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) = ( 1 · ( vol ‘ 𝐴 ) ) )
62 simplr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ 𝐴 ) ∈ ℝ )
63 62 recnd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( vol ‘ 𝐴 ) ∈ ℂ )
64 63 mullidd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ 𝐴 ) ) = ( vol ‘ 𝐴 ) )
65 61 64 eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) = ( vol ‘ 𝐴 ) )
66 65 63 eqeltrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ∈ ℂ )
67 id ⊢ ( 𝑧 = 1 → 𝑧 = 1 )
68 sneq ⊢ ( 𝑧 = 1 → { 𝑧 } = { 1 } )
69 68 imaeq2d ⊢ ( 𝑧 = 1 → ( ◡ 𝐹 “ { 𝑧 } ) = ( ◡ 𝐹 “ { 1 } ) )
70 69 fveq2d ⊢ ( 𝑧 = 1 → ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) = ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) )
71 67 70 oveq12d ⊢ ( 𝑧 = 1 → ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) )
72 71 sumsn ⊢ ( ( 1 ∈ ℝ ∧ ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) ∈ ℂ ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) )
73 57 66 72 sylancr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( 1 · ( vol ‘ ( ◡ 𝐹 “ { 1 } ) ) ) )
74 73 65 eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ { 1 } ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( vol ‘ 𝐴 ) )
75 56 74 eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → Σ 𝑧 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐹 “ { 𝑧 } ) ) ) = ( vol ‘ 𝐴 ) )
76 23 75 eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) )
77 76 ex ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝑦 ∈ 𝐴 → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) )
78 77 exlimdv ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∃ 𝑦 𝑦 ∈ 𝐴 → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) )
79 19 78 biimtrid ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 ≠ ∅ → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) ) )
80 18 79 pm2.61dne ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1 ‘ 𝐹 ) = ( vol ‘ 𝐴 ) )