# Metamath Proof Explorer

## Theorem ovnprodcl

Description: The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

### Proof

Step Hyp Ref Expression
1 ovnprodcl.kph
` |-  F/ k ph`
2 ovnprodcl.x
` |-  ( ph -> X e. Fin )`
3 ovnprodcl.f
` |-  ( ph -> F : NN --> ( ( RR X. RR ) ^m X ) )`
4 ovnprodcl.i
` |-  ( ph -> I e. NN )`
5 3 4 ffvelrnd
` |-  ( ph -> ( F ` I ) e. ( ( RR X. RR ) ^m X ) )`
6 elmapi
` |-  ( ( F ` I ) e. ( ( RR X. RR ) ^m X ) -> ( F ` I ) : X --> ( RR X. RR ) )`
7 5 6 syl
` |-  ( ph -> ( F ` I ) : X --> ( RR X. RR ) )`
8 1 2 7 hoiprodcl
` |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. ( F ` I ) ) ` k ) ) e. ( 0 [,) +oo ) )`