This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg10a

Description: The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg10a.1 
|- ( ph -> F e. dom S.1 )
itg10a.2 
|- ( ph -> A C_ RR )
itg10a.3 
|- ( ph -> ( vol* ` A ) = 0 )
itg10a.4 
|- ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = 0 )
Assertion itg10a 
|- ( ph -> ( S.1 ` F ) = 0 )

Proof

Step Hyp Ref Expression
1 itg10a.1 
 |-  ( ph -> F e. dom S.1 )
2 itg10a.2 
 |-  ( ph -> A C_ RR )
3 itg10a.3 
 |-  ( ph -> ( vol* ` A ) = 0 )
4 itg10a.4 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> ( F ` x ) = 0 )
5 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
6 1 5 syl 
 |-  ( ph -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
7 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
8 1 7 syl 
 |-  ( ph -> F : RR --> RR )
9 8 ffnd 
 |-  ( ph -> F Fn RR )
10 9 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> F Fn RR )
11 fniniseg 
 |-  ( F Fn RR -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
12 10 11 syl 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
13 eldifsni 
 |-  ( k e. ( ran F \ { 0 } ) -> k =/= 0 )
14 13 ad2antlr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> k =/= 0 )
15 simprl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> x e. RR )
16 eldif 
 |-  ( x e. ( RR \ A ) <-> ( x e. RR /\ -. x e. A ) )
17 simplrr 
 |-  ( ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) /\ x e. ( RR \ A ) ) -> ( F ` x ) = k )
18 4 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) /\ x e. ( RR \ A ) ) -> ( F ` x ) = 0 )
19 17 18 eqtr3d 
 |-  ( ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) /\ x e. ( RR \ A ) ) -> k = 0 )
20 19 ex 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( x e. ( RR \ A ) -> k = 0 ) )
21 16 20 biimtrrid 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( ( x e. RR /\ -. x e. A ) -> k = 0 ) )
22 15 21 mpand 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( -. x e. A -> k = 0 ) )
23 22 necon1ad 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( k =/= 0 -> x e. A ) )
24 14 23 mpd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> x e. A )
25 24 ex 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( ( x e. RR /\ ( F ` x ) = k ) -> x e. A ) )
26 12 25 sylbid 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( x e. ( `' F " { k } ) -> x e. A ) )
27 26 ssrdv 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) C_ A )
28 2 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> A C_ RR )
29 27 28 sstrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) C_ RR )
30 3 adantr 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol* ` A ) = 0 )
31 ovolssnul 
 |-  ( ( ( `' F " { k } ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( `' F " { k } ) ) = 0 )
32 27 28 30 31 syl3anc 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol* ` ( `' F " { k } ) ) = 0 )
33 nulmbl 
 |-  ( ( ( `' F " { k } ) C_ RR /\ ( vol* ` ( `' F " { k } ) ) = 0 ) -> ( `' F " { k } ) e. dom vol )
34 29 32 33 syl2anc 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( `' F " { k } ) e. dom vol )
35 mblvol 
 |-  ( ( `' F " { k } ) e. dom vol -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
36 34 35 syl 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
37 36 32 eqtrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) = 0 )
38 37 oveq2d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) = ( k x. 0 ) )
39 8 frnd 
 |-  ( ph -> ran F C_ RR )
40 39 ssdifssd 
 |-  ( ph -> ( ran F \ { 0 } ) C_ RR )
41 40 sselda 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. RR )
42 41 recnd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. CC )
43 42 mul01d 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( k x. 0 ) = 0 )
44 38 43 eqtrd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) = 0 )
45 44 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) = sum_ k e. ( ran F \ { 0 } ) 0 )
46 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
47 1 46 syl 
 |-  ( ph -> ran F e. Fin )
48 difss 
 |-  ( ran F \ { 0 } ) C_ ran F
49 ssfi 
 |-  ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin )
50 47 48 49 sylancl 
 |-  ( ph -> ( ran F \ { 0 } ) e. Fin )
51 50 olcd 
 |-  ( ph -> ( ( ran F \ { 0 } ) C_ ( ZZ>= ` 0 ) \/ ( ran F \ { 0 } ) e. Fin ) )
52 sumz 
 |-  ( ( ( ran F \ { 0 } ) C_ ( ZZ>= ` 0 ) \/ ( ran F \ { 0 } ) e. Fin ) -> sum_ k e. ( ran F \ { 0 } ) 0 = 0 )
53 51 52 syl 
 |-  ( ph -> sum_ k e. ( ran F \ { 0 } ) 0 = 0 )
54 45 53 eqtrd 
 |-  ( ph -> sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) = 0 )
55 6 54 eqtrd 
 |-  ( ph -> ( S.1 ` F ) = 0 )