Metamath Proof Explorer

Theorem hoiprodcl2

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

Ref Expression
Hypotheses hoiprodcl2.kph 
|- F/ k ph
hoiprodcl2.x 
|- ( ph -> X e. Fin )
hoiprodcl2.l 
|- L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
hoiprodcl2.i 
|- ( ph -> I : X --> ( RR X. RR ) )
Assertion hoiprodcl2 
|- ( ph -> ( L ` I ) e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 hoiprodcl2.kph 
 |-  F/ k ph
2 hoiprodcl2.x 
 |-  ( ph -> X e. Fin )
3 hoiprodcl2.l 
 |-  L = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) )
4 hoiprodcl2.i 
 |-  ( ph -> I : X --> ( RR X. RR ) )
5 coeq2 
 |-  ( i = I -> ( [,) o. i ) = ( [,) o. I ) )
6 5 fveq1d 
 |-  ( i = I -> ( ( [,) o. i ) ` k ) = ( ( [,) o. I ) ` k ) )
7 6 fveq2d 
 |-  ( i = I -> ( vol ` ( ( [,) o. i ) ` k ) ) = ( vol ` ( ( [,) o. I ) ` k ) ) )
8 7 ralrimivw 
 |-  ( i = I -> A. k e. X ( vol ` ( ( [,) o. i ) ` k ) ) = ( vol ` ( ( [,) o. I ) ` k ) ) )
9 8 prodeq2d 
 |-  ( i = I -> prod_ k e. X ( vol ` ( ( [,) o. i ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) )
10 reex 
 |-  RR e. _V
11 10 10 xpex 
 |-  ( RR X. RR ) e. _V
12 11 a1i 
 |-  ( ph -> ( RR X. RR ) e. _V )
13 12 2 jca 
 |-  ( ph -> ( ( RR X. RR ) e. _V /\ X e. Fin ) )
14 elmapg 
 |-  ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( I e. ( ( RR X. RR ) ^m X ) <-> I : X --> ( RR X. RR ) ) )
15 13 14 syl 
 |-  ( ph -> ( I e. ( ( RR X. RR ) ^m X ) <-> I : X --> ( RR X. RR ) ) )
16 4 15 mpbird 
 |-  ( ph -> I e. ( ( RR X. RR ) ^m X ) )
17 1 2 4 hoiprodcl 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) e. ( 0 [,) +oo ) )
18 3 9 16 17 fvmptd3 
 |-  ( ph -> ( L ` I ) = prod_ k e. X ( vol ` ( ( [,) o. I ) ` k ) ) )
19 18 17 eqeltrd 
 |-  ( ph -> ( L ` I ) e. ( 0 [,) +oo ) )