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