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 ) )