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

Metamath Proof Explorer

Theorem itgvol0

Description: If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgvol0.1 
|- ( ph -> A C_ RR )
itgvol0.2 
|- ( ph -> ( vol* ` A ) = 0 )
itgvol0.3 
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion itgvol0 
|- ( ph -> ( ( x e. A |-> B ) e. L^1 /\ S. A B _d x = 0 ) )

Proof

Step Hyp Ref Expression
1 itgvol0.1 
 |-  ( ph -> A C_ RR )
2 itgvol0.2 
 |-  ( ph -> ( vol* ` A ) = 0 )
3 itgvol0.3 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
4 mpt0 
 |-  ( x e. (/) |-> B ) = (/)
5 iblempty 
 |-  (/) e. L^1
6 4 5 eqeltri 
 |-  ( x e. (/) |-> B ) e. L^1
7 0ss 
 |-  (/) C_ A
8 7 a1i 
 |-  ( ph -> (/) C_ A )
9 difssd 
 |-  ( ph -> ( A \ (/) ) C_ A )
10 ovolssnul 
 |-  ( ( ( A \ (/) ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( A \ (/) ) ) = 0 )
11 9 1 2 10 syl3anc 
 |-  ( ph -> ( vol* ` ( A \ (/) ) ) = 0 )
12 8 1 11 3 itgss3 
 |-  ( ph -> ( ( ( x e. (/) |-> B ) e. L^1 <-> ( x e. A |-> B ) e. L^1 ) /\ S. (/) B _d x = S. A B _d x ) )
13 12 simpld 
 |-  ( ph -> ( ( x e. (/) |-> B ) e. L^1 <-> ( x e. A |-> B ) e. L^1 ) )
14 6 13 mpbii 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
15 12 simprd 
 |-  ( ph -> S. (/) B _d x = S. A B _d x )
16 itg0 
 |-  S. (/) B _d x = 0
17 15 16 eqtr3di 
 |-  ( ph -> S. A B _d x = 0 )
18 14 17 jca 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 /\ S. A B _d x = 0 ) )