Metamath Proof Explorer

Theorem itg1val2

Description: The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion itg1val2 
|- ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` F ) = sum_ x e. A ( x x. ( vol ` ( `' F " { x } ) ) ) )

Proof

Step Hyp Ref Expression
1 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
2 1 adantr 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) )
3 simpr2 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> ( ran F \ { 0 } ) C_ A )
4 3 sselda 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( ran F \ { 0 } ) ) -> x e. A )
5 simpr3 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> A C_ ( RR \ { 0 } ) )
6 5 sselda 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. A ) -> x e. ( RR \ { 0 } ) )
7 eldifi 
 |-  ( x e. ( RR \ { 0 } ) -> x e. RR )
8 6 7 syl 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. A ) -> x e. RR )
9 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ x e. ( RR \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
10 9 adantlr 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( RR \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
11 6 10 syldan 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. A ) -> ( vol ` ( `' F " { x } ) ) e. RR )
12 8 11 remulcld 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. A ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR )
13 12 recnd 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. A ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. CC )
14 4 13 syldan 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( ran F \ { 0 } ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. CC )
15 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
16 15 ad2antrr 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> F : RR --> RR )
17 ffrn 
 |-  ( F : RR --> RR -> F : RR --> ran F )
18 16 17 syl 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> F : RR --> ran F )
19 eldifn 
 |-  ( x e. ( A \ ( ran F \ { 0 } ) ) -> -. x e. ( ran F \ { 0 } ) )
20 19 adantl 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> -. x e. ( ran F \ { 0 } ) )
21 eldif 
 |-  ( x e. ( ran F \ { 0 } ) <-> ( x e. ran F /\ -. x e. { 0 } ) )
22 simplr3 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> A C_ ( RR \ { 0 } ) )
23 22 ssdifssd 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( A \ ( ran F \ { 0 } ) ) C_ ( RR \ { 0 } ) )
24 simpr 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> x e. ( A \ ( ran F \ { 0 } ) ) )
25 23 24 sseldd 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> x e. ( RR \ { 0 } ) )
26 eldifn 
 |-  ( x e. ( RR \ { 0 } ) -> -. x e. { 0 } )
27 25 26 syl 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> -. x e. { 0 } )
28 27 biantrud 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( x e. ran F <-> ( x e. ran F /\ -. x e. { 0 } ) ) )
29 21 28 bitr4id 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( x e. ( ran F \ { 0 } ) <-> x e. ran F ) )
30 20 29 mtbid 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> -. x e. ran F )
31 disjsn 
 |-  ( ( ran F i^i { x } ) = (/) <-> -. x e. ran F )
32 30 31 sylibr 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( ran F i^i { x } ) = (/) )
33 fimacnvdisj 
 |-  ( ( F : RR --> ran F /\ ( ran F i^i { x } ) = (/) ) -> ( `' F " { x } ) = (/) )
34 18 32 33 syl2anc 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( `' F " { x } ) = (/) )
35 34 fveq2d 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( vol ` ( `' F " { x } ) ) = ( vol ` (/) ) )
36 0mbl 
 |-  (/) e. dom vol
37 mblvol 
 |-  ( (/) e. 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 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( vol ` ( `' F " { x } ) ) = 0 )
42 41 oveq2d 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) = ( x x. 0 ) )
43 eldifi 
 |-  ( x e. ( A \ ( ran F \ { 0 } ) ) -> x e. A )
44 43 8 sylan2 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> x e. RR )
45 44 recnd 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> x e. CC )
46 45 mul01d 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( x x. 0 ) = 0 )
47 42 46 eqtrd 
 |-  ( ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) /\ x e. ( A \ ( ran F \ { 0 } ) ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) = 0 )
48 simpr1 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> A e. Fin )
49 3 14 47 48 fsumss 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) = sum_ x e. A ( x x. ( vol ` ( `' F " { x } ) ) ) )
50 2 49 eqtrd 
 |-  ( ( F e. dom S.1 /\ ( A e. Fin /\ ( ran F \ { 0 } ) C_ A /\ A C_ ( RR \ { 0 } ) ) ) -> ( S.1 ` F ) = sum_ x e. A ( x x. ( vol ` ( `' F " { x } ) ) ) )