# 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 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
hoiprodcl2.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
hoiprodcl2.l ${⊢}{L}=\left({i}\in \left({{ℝ}^{2}}^{{X}}\right)⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\right)\left({k}\right)\right)\right)$
hoiprodcl2.i ${⊢}{\phi }\to {I}:{X}⟶{ℝ}^{2}$
Assertion hoiprodcl2 ${⊢}{\phi }\to {L}\left({I}\right)\in \left[0,\mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 hoiprodcl2.kph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 hoiprodcl2.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
3 hoiprodcl2.l ${⊢}{L}=\left({i}\in \left({{ℝ}^{2}}^{{X}}\right)⟼\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\right)\left({k}\right)\right)\right)$
4 hoiprodcl2.i ${⊢}{\phi }\to {I}:{X}⟶{ℝ}^{2}$
5 coeq2 ${⊢}{i}={I}\to \left[.\right)\circ {i}=\left[.\right)\circ {I}$
6 5 fveq1d ${⊢}{i}={I}\to \left(\left[.\right)\circ {i}\right)\left({k}\right)=\left(\left[.\right)\circ {I}\right)\left({k}\right)$
7 6 fveq2d ${⊢}{i}={I}\to vol\left(\left(\left[.\right)\circ {i}\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
8 7 ralrimivw ${⊢}{i}={I}\to \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}vol\left(\left(\left[.\right)\circ {i}\right)\left({k}\right)\right)=vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
9 8 prodeq2d ${⊢}{i}={I}\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {i}\right)\left({k}\right)\right)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
10 reex ${⊢}ℝ\in \mathrm{V}$
11 10 10 xpex ${⊢}{ℝ}^{2}\in \mathrm{V}$
12 11 a1i ${⊢}{\phi }\to {ℝ}^{2}\in \mathrm{V}$
13 12 2 jca ${⊢}{\phi }\to \left({ℝ}^{2}\in \mathrm{V}\wedge {X}\in \mathrm{Fin}\right)$
14 elmapg ${⊢}\left({ℝ}^{2}\in \mathrm{V}\wedge {X}\in \mathrm{Fin}\right)\to \left({I}\in \left({{ℝ}^{2}}^{{X}}\right)↔{I}:{X}⟶{ℝ}^{2}\right)$
15 13 14 syl ${⊢}{\phi }\to \left({I}\in \left({{ℝ}^{2}}^{{X}}\right)↔{I}:{X}⟶{ℝ}^{2}\right)$
16 4 15 mpbird ${⊢}{\phi }\to {I}\in \left({{ℝ}^{2}}^{{X}}\right)$
17 1 2 4 hoiprodcl ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)\in \left[0,\mathrm{+\infty }\right)$
18 3 9 16 17 fvmptd3 ${⊢}{\phi }\to {L}\left({I}\right)=\prod _{{k}\in {X}}vol\left(\left(\left[.\right)\circ {I}\right)\left({k}\right)\right)$
19 18 17 eqeltrd ${⊢}{\phi }\to {L}\left({I}\right)\in \left[0,\mathrm{+\infty }\right)$