# Metamath Proof Explorer

## Theorem hoiprodp1

Description: The dimensional volume of a half-open interval with dimension n + 1 . Used in the first equality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoiprodp1.l ${⊢}{L}=\left({x}\in \mathrm{Fin}⟼\left({a}\in \left({ℝ}^{{x}}\right),{b}\in \left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,\prod _{{k}\in {x}}vol\left(\left[{a}\left({k}\right),{b}\left({k}\right)\right)\right)\right)\right)\right)$
hoiprodp1.y ${⊢}{\phi }\to {Y}\in \mathrm{Fin}$
hoiprodp1.3 ${⊢}{\phi }\to {Z}\in {V}$
hoiprodp1.z ${⊢}{\phi }\to ¬{Z}\in {Y}$
hoiprodp1.x ${⊢}{X}={Y}\cup \left\{{Z}\right\}$
hoiprodp1.a ${⊢}{\phi }\to {A}:{X}⟶ℝ$
hoiprodp1.b ${⊢}{\phi }\to {B}:{X}⟶ℝ$
hoiprodp1.g ${⊢}{G}=\prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)$
Assertion hoiprodp1 ${⊢}{\phi }\to {A}{L}\left({X}\right){B}={G}vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 hoiprodp1.l ${⊢}{L}=\left({x}\in \mathrm{Fin}⟼\left({a}\in \left({ℝ}^{{x}}\right),{b}\in \left({ℝ}^{{x}}\right)⟼if\left({x}=\varnothing ,0,\prod _{{k}\in {x}}vol\left(\left[{a}\left({k}\right),{b}\left({k}\right)\right)\right)\right)\right)\right)$
2 hoiprodp1.y ${⊢}{\phi }\to {Y}\in \mathrm{Fin}$
3 hoiprodp1.3 ${⊢}{\phi }\to {Z}\in {V}$
4 hoiprodp1.z ${⊢}{\phi }\to ¬{Z}\in {Y}$
5 hoiprodp1.x ${⊢}{X}={Y}\cup \left\{{Z}\right\}$
6 hoiprodp1.a ${⊢}{\phi }\to {A}:{X}⟶ℝ$
7 hoiprodp1.b ${⊢}{\phi }\to {B}:{X}⟶ℝ$
8 hoiprodp1.g ${⊢}{G}=\prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)$
9 snfi ${⊢}\left\{{Z}\right\}\in \mathrm{Fin}$
10 9 a1i ${⊢}{\phi }\to \left\{{Z}\right\}\in \mathrm{Fin}$
11 unfi ${⊢}\left({Y}\in \mathrm{Fin}\wedge \left\{{Z}\right\}\in \mathrm{Fin}\right)\to {Y}\cup \left\{{Z}\right\}\in \mathrm{Fin}$
12 2 10 11 syl2anc ${⊢}{\phi }\to {Y}\cup \left\{{Z}\right\}\in \mathrm{Fin}$
13 5 12 eqeltrid ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
14 snidg ${⊢}{Z}\in {V}\to {Z}\in \left\{{Z}\right\}$
15 3 14 syl ${⊢}{\phi }\to {Z}\in \left\{{Z}\right\}$
16 elun2 ${⊢}{Z}\in \left\{{Z}\right\}\to {Z}\in \left({Y}\cup \left\{{Z}\right\}\right)$
17 15 16 syl ${⊢}{\phi }\to {Z}\in \left({Y}\cup \left\{{Z}\right\}\right)$
18 17 5 eleqtrrdi ${⊢}{\phi }\to {Z}\in {X}$
19 18 ne0d ${⊢}{\phi }\to {X}\ne \varnothing$
20 1 13 19 6 7 hoidmvn0val ${⊢}{\phi }\to {A}{L}\left({X}\right){B}=\prod _{{k}\in {X}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)$
21 6 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {A}\left({k}\right)\in ℝ$
22 7 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {B}\left({k}\right)\in ℝ$
23 volicore ${⊢}\left({A}\left({k}\right)\in ℝ\wedge {B}\left({k}\right)\in ℝ\right)\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\in ℝ$
24 21 22 23 syl2anc ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\in ℝ$
25 24 recnd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\in ℂ$
26 fveq2 ${⊢}{k}={Z}\to {A}\left({k}\right)={A}\left({Z}\right)$
27 fveq2 ${⊢}{k}={Z}\to {B}\left({k}\right)={B}\left({Z}\right)$
28 26 27 oveq12d ${⊢}{k}={Z}\to \left[{A}\left({k}\right),{B}\left({k}\right)\right)=\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)$
29 28 fveq2d ${⊢}{k}={Z}\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)=vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$
30 29 adantl ${⊢}\left({\phi }\wedge {k}={Z}\right)\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)=vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$
31 13 25 18 30 fprodsplit1 ${⊢}{\phi }\to \prod _{{k}\in {X}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)=vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\prod _{{k}\in {X}\setminus \left\{{Z}\right\}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)$
32 5 difeq1i ${⊢}{X}\setminus \left\{{Z}\right\}=\left({Y}\cup \left\{{Z}\right\}\right)\setminus \left\{{Z}\right\}$
33 32 a1i ${⊢}{\phi }\to {X}\setminus \left\{{Z}\right\}=\left({Y}\cup \left\{{Z}\right\}\right)\setminus \left\{{Z}\right\}$
34 difun2 ${⊢}\left({Y}\cup \left\{{Z}\right\}\right)\setminus \left\{{Z}\right\}={Y}\setminus \left\{{Z}\right\}$
35 34 a1i ${⊢}{\phi }\to \left({Y}\cup \left\{{Z}\right\}\right)\setminus \left\{{Z}\right\}={Y}\setminus \left\{{Z}\right\}$
36 difsn ${⊢}¬{Z}\in {Y}\to {Y}\setminus \left\{{Z}\right\}={Y}$
37 4 36 syl ${⊢}{\phi }\to {Y}\setminus \left\{{Z}\right\}={Y}$
38 33 35 37 3eqtrd ${⊢}{\phi }\to {X}\setminus \left\{{Z}\right\}={Y}$
39 38 prodeq1d ${⊢}{\phi }\to \prod _{{k}\in {X}\setminus \left\{{Z}\right\}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)=\prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)$
40 8 eqcomi ${⊢}\prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)={G}$
41 40 a1i ${⊢}{\phi }\to \prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)={G}$
42 39 41 eqtrd ${⊢}{\phi }\to \prod _{{k}\in {X}\setminus \left\{{Z}\right\}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)={G}$
43 42 oveq2d ${⊢}{\phi }\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\prod _{{k}\in {X}\setminus \left\{{Z}\right\}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)=vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right){G}$
44 6 18 ffvelrnd ${⊢}{\phi }\to {A}\left({Z}\right)\in ℝ$
45 7 18 ffvelrnd ${⊢}{\phi }\to {B}\left({Z}\right)\in ℝ$
46 volicore ${⊢}\left({A}\left({Z}\right)\in ℝ\wedge {B}\left({Z}\right)\in ℝ\right)\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\in ℝ$
47 44 45 46 syl2anc ${⊢}{\phi }\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\in ℝ$
48 47 recnd ${⊢}{\phi }\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\in ℂ$
49 6 adantr ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to {A}:{X}⟶ℝ$
50 ssun1 ${⊢}{Y}\subseteq {Y}\cup \left\{{Z}\right\}$
51 50 5 sseqtrri ${⊢}{Y}\subseteq {X}$
52 id ${⊢}{k}\in {Y}\to {k}\in {Y}$
53 51 52 sseldi ${⊢}{k}\in {Y}\to {k}\in {X}$
54 53 adantl ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to {k}\in {X}$
55 49 54 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to {A}\left({k}\right)\in ℝ$
56 7 adantr ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to {B}:{X}⟶ℝ$
57 56 54 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to {B}\left({k}\right)\in ℝ$
58 55 57 23 syl2anc ${⊢}\left({\phi }\wedge {k}\in {Y}\right)\to vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\in ℝ$
59 2 58 fprodrecl ${⊢}{\phi }\to \prod _{{k}\in {Y}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\in ℝ$
60 8 59 eqeltrid ${⊢}{\phi }\to {G}\in ℝ$
61 60 recnd ${⊢}{\phi }\to {G}\in ℂ$
62 48 61 mulcomd ${⊢}{\phi }\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right){G}={G}vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$
63 43 62 eqtrd ${⊢}{\phi }\to vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)\prod _{{k}\in {X}\setminus \left\{{Z}\right\}}vol\left(\left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)={G}vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$
64 20 31 63 3eqtrd ${⊢}{\phi }\to {A}{L}\left({X}\right){B}={G}vol\left(\left[{A}\left({Z}\right),{B}\left({Z}\right)\right)\right)$