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 mulid2d ( ( ( 𝐴 ∈ 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 syl5bi ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 ≠ ∅ → ( ∫1𝐹 ) = ( vol ‘ 𝐴 ) ) )
80 18 79 pm2.61dne ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ∫1𝐹 ) = ( vol ‘ 𝐴 ) )