Metamath Proof Explorer

Theorem hoiprodcl

Description: The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoiprodcl.1 
|- F/ k ph
hoiprodcl.2 
|- ( ph -> X e. Fin )
hoiprodcl.3 
|- ( ph -> I : X --> ( RR X. RR ) )
Assertion hoiprodcl 
|- ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 hoiprodcl.1 
 |-  F/ k ph
2 hoiprodcl.2 
 |-  ( ph -> X e. Fin )
3 hoiprodcl.3 
 |-  ( ph -> I : X --> ( RR X. RR ) )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( ph -> 0 e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 6 a1i 
 |-  ( ph -> +oo e. RR* )
8 3 adantr 
 |-  ( ( ph /\ k e. X ) -> I : X --> ( RR X. RR ) )
9 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
10 8 9 fvovco 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) = ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) )
11 10 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) = ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) )
12 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( I ` k ) e. ( RR X. RR ) )
13 xp1st 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 1st ` ( I ` k ) ) e. RR )
14 12 13 syl 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( I ` k ) ) e. RR )
15 xp2nd 
 |-  ( ( I ` k ) e. ( RR X. RR ) -> ( 2nd ` ( I ` k ) ) e. RR )
16 12 15 syl 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR )
17 volico 
 |-  ( ( ( 1st ` ( I ` k ) ) e. RR /\ ( 2nd ` ( I ` k ) ) e. RR ) -> ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )
18 14 16 17 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )
19 11 18 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) = if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) )
20 16 14 resubcld 
 |-  ( ( ph /\ k e. X ) -> ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) e. RR )
21 0red 
 |-  ( ( ph /\ k e. X ) -> 0 e. RR )
22 20 21 ifcld 
 |-  ( ( ph /\ k e. X ) -> if ( ( 1st ` ( I ` k ) ) < ( 2nd ` ( I ` k ) ) , ( ( 2nd ` ( I ` k ) ) - ( 1st ` ( I ` k ) ) ) , 0 ) e. RR )
23 19 22 eqeltrd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. I ) ` k ) ) e. RR )
24 1 2 23 fprodreclf 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. RR )
25 24 rexrd 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. RR* )
26 16 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( I ` k ) ) e. RR* )
27 icombl 
 |-  ( ( ( 1st ` ( I ` k ) ) e. RR /\ ( 2nd ` ( I ` k ) ) e. RR* ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) e. dom vol )
28 14 26 27 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( I ` k ) ) [,) ( 2nd ` ( I ` k ) ) ) e. dom vol )
29 10 28 eqeltrd 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. I ) ` k ) e. dom vol )
30 volge0 
 |-  ( ( ( [,) o. I ) ` k ) e. dom vol -> 0 <_ ( vol ` ( ( [,) o. I ) ` k ) ) )
31 29 30 syl 
 |-  ( ( ph /\ k e. X ) -> 0 <_ ( vol ` ( ( [,) o. I ) ` k ) ) )
32 1 2 23 31 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) )
33 24 ltpnfd 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) < +oo )
34 5 7 25 32 33 elicod 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )