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 
|- F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
Assertion itg11 
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( S.1 ` F ) = ( vol ` A ) )

Proof

Step Hyp Ref Expression
1 i1f1.1 
 |-  F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
2 ovol0 
 |-  ( vol* ` (/) ) = 0
3 0mbl 
 |-  (/) e. dom vol
4 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
5 3 4 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
6 itg10 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = 0
7 2 5 6 3eqtr4ri 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = ( vol ` (/) )
8 noel 
 |-  -. x e. (/)
9 eleq2 
 |-  ( A = (/) -> ( x e. A <-> x e. (/) ) )
10 8 9 mtbiri 
 |-  ( A = (/) -> -. x e. A )
11 10 iffalsed 
 |-  ( A = (/) -> if ( x e. A , 1 , 0 ) = 0 )
12 11 mpteq2dv 
 |-  ( A = (/) -> ( x e. RR |-> if ( x e. A , 1 , 0 ) ) = ( x e. RR |-> 0 ) )
13 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
14 12 1 13 3eqtr4g 
 |-  ( A = (/) -> F = ( RR X. { 0 } ) )
15 14 fveq2d 
 |-  ( A = (/) -> ( S.1 ` F ) = ( S.1 ` ( RR X. { 0 } ) ) )
16 fveq2 
 |-  ( A = (/) -> ( vol ` A ) = ( vol ` (/) ) )
17 7 15 16 3eqtr4a 
 |-  ( A = (/) -> ( S.1 ` F ) = ( vol ` A ) )
18 17 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( A = (/) -> ( S.1 ` F ) = ( vol ` A ) ) )
19 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
20 1 i1f1 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F e. dom S.1 )
21 20 adantr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> F e. dom S.1 )
22 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ z e. ( ran F \ { 0 } ) ( z x. ( vol ` ( `' F " { z } ) ) ) )
23 21 22 syl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( S.1 ` F ) = sum_ z e. ( ran F \ { 0 } ) ( z x. ( vol ` ( `' F " { z } ) ) ) )
24 1 i1f1lem 
 |-  ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )
25 24 simpli 
 |-  F : RR --> { 0 , 1 }
26 frn 
 |-  ( F : RR --> { 0 , 1 } -> ran F C_ { 0 , 1 } )
27 25 26 ax-mp 
 |-  ran F C_ { 0 , 1 }
28 ssdif 
 |-  ( ran F C_ { 0 , 1 } -> ( ran F \ { 0 } ) C_ ( { 0 , 1 } \ { 0 } ) )
29 27 28 ax-mp 
 |-  ( ran F \ { 0 } ) C_ ( { 0 , 1 } \ { 0 } )
30 difprsnss 
 |-  ( { 0 , 1 } \ { 0 } ) C_ { 1 }
31 29 30 sstri 
 |-  ( ran F \ { 0 } ) C_ { 1 }
32 31 a1i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( ran F \ { 0 } ) C_ { 1 } )
33 mblss 
 |-  ( A e. dom vol -> A C_ RR )
34 33 adantr 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A C_ RR )
35 34 sselda 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> y e. RR )
36 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
37 36 ifbid 
 |-  ( x = y -> if ( x e. A , 1 , 0 ) = if ( y e. A , 1 , 0 ) )
38 1ex 
 |-  1 e. _V
39 c0ex 
 |-  0 e. _V
40 38 39 ifex 
 |-  if ( y e. A , 1 , 0 ) e. _V
41 37 1 40 fvmpt 
 |-  ( y e. RR -> ( F ` y ) = if ( y e. A , 1 , 0 ) )
42 35 41 syl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( F ` y ) = if ( y e. A , 1 , 0 ) )
43 iftrue 
 |-  ( y e. A -> if ( y e. A , 1 , 0 ) = 1 )
44 43 adantl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> if ( y e. A , 1 , 0 ) = 1 )
45 42 44 eqtrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( F ` y ) = 1 )
46 ffn 
 |-  ( F : RR --> { 0 , 1 } -> F Fn RR )
47 25 46 ax-mp 
 |-  F Fn RR
48 fnfvelrn 
 |-  ( ( F Fn RR /\ y e. RR ) -> ( F ` y ) e. ran F )
49 47 35 48 sylancr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( F ` y ) e. ran F )
50 45 49 eqeltrrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> 1 e. ran F )
51 ax-1ne0 
 |-  1 =/= 0
52 eldifsn 
 |-  ( 1 e. ( ran F \ { 0 } ) <-> ( 1 e. ran F /\ 1 =/= 0 ) )
53 50 51 52 sylanblrc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> 1 e. ( ran F \ { 0 } ) )
54 53 snssd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> { 1 } C_ ( ran F \ { 0 } ) )
55 32 54 eqssd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( ran F \ { 0 } ) = { 1 } )
56 55 sumeq1d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> sum_ z e. ( ran F \ { 0 } ) ( z x. ( vol ` ( `' F " { z } ) ) ) = sum_ z e. { 1 } ( z x. ( vol ` ( `' F " { z } ) ) ) )
57 1re 
 |-  1 e. RR
58 24 simpri 
 |-  ( A e. dom vol -> ( `' F " { 1 } ) = A )
59 58 ad2antrr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( `' F " { 1 } ) = A )
60 59 fveq2d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( vol ` ( `' F " { 1 } ) ) = ( vol ` A ) )
61 60 oveq2d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) = ( 1 x. ( vol ` A ) ) )
62 simplr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( vol ` A ) e. RR )
63 62 recnd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( vol ` A ) e. CC )
64 63 mulid2d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( 1 x. ( vol ` A ) ) = ( vol ` A ) )
65 61 64 eqtrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) = ( vol ` A ) )
66 65 63 eqeltrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) e. CC )
67 id 
 |-  ( z = 1 -> z = 1 )
68 sneq 
 |-  ( z = 1 -> { z } = { 1 } )
69 68 imaeq2d 
 |-  ( z = 1 -> ( `' F " { z } ) = ( `' F " { 1 } ) )
70 69 fveq2d 
 |-  ( z = 1 -> ( vol ` ( `' F " { z } ) ) = ( vol ` ( `' F " { 1 } ) ) )
71 67 70 oveq12d 
 |-  ( z = 1 -> ( z x. ( vol ` ( `' F " { z } ) ) ) = ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) )
72 71 sumsn 
 |-  ( ( 1 e. RR /\ ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) e. CC ) -> sum_ z e. { 1 } ( z x. ( vol ` ( `' F " { z } ) ) ) = ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) )
73 57 66 72 sylancr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> sum_ z e. { 1 } ( z x. ( vol ` ( `' F " { z } ) ) ) = ( 1 x. ( vol ` ( `' F " { 1 } ) ) ) )
74 73 65 eqtrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> sum_ z e. { 1 } ( z x. ( vol ` ( `' F " { z } ) ) ) = ( vol ` A ) )
75 56 74 eqtrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> sum_ z e. ( ran F \ { 0 } ) ( z x. ( vol ` ( `' F " { z } ) ) ) = ( vol ` A ) )
76 23 75 eqtrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. A ) -> ( S.1 ` F ) = ( vol ` A ) )
77 76 ex 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( y e. A -> ( S.1 ` F ) = ( vol ` A ) ) )
78 77 exlimdv 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( E. y y e. A -> ( S.1 ` F ) = ( vol ` A ) ) )
79 19 78 syl5bi 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( A =/= (/) -> ( S.1 ` F ) = ( vol ` A ) ) )
80 18 79 pm2.61dne 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( S.1 ` F ) = ( vol ` A ) )