vonn0ioo2

Description: The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonn0ioo2.k	$⊢ Ⅎ k φ$
	vonn0ioo2.x	$⊢ φ \to X \in Fin$
	vonn0ioo2.n	$⊢ φ \to X \neq \emptyset$
	vonn0ioo2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	vonn0ioo2.b	$⊢ (φ \land k \in X) \to B \in ℝ$
	vonn0ioo2.i	$⊢ I = \underset{k \in X}{⨉} (A, B)$
Assertion	vonn0ioo2	$⊢ φ \to voln (X) (I) = \prod_{k \in X} vol ((A, B))$

Proof

Step	Hyp	Ref	Expression
1		vonn0ioo2.k	$⊢ Ⅎ k φ$
2		vonn0ioo2.x	$⊢ φ \to X \in Fin$
3		vonn0ioo2.n	$⊢ φ \to X \neq \emptyset$
4		vonn0ioo2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
5		vonn0ioo2.b	$⊢ (φ \land k \in X) \to B \in ℝ$
6		vonn0ioo2.i	$⊢ I = \underset{k \in X}{⨉} (A, B)$
7	6	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} (A, B)$
8		simpr	$⊢ (φ \land j \in X) \to j \in X$
9		nfv	$⊢ Ⅎ k j \in X$
10	1 9	nfan	$⊢ Ⅎ k (φ \land j \in X)$
11		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
12		nfcv	$⊢ \underline{Ⅎ} k ℝ$
13	11 12	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ A \in ℝ$
14	10 13	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ)$
15		eleq1w	$⊢ k = j \to (k \in X \leftrightarrow j \in X)$
16	15	anbi2d	$⊢ k = j \to ((φ \land k \in X) \leftrightarrow (φ \land j \in X))$
17		csbeq1a	$⊢ k = j \to A = ⦋ j / k ⦌ A$
18	17	eleq1d	$⊢ k = j \to (A \in ℝ \leftrightarrow ⦋ j / k ⦌ A \in ℝ)$
19	16 18	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to A \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ))$
20	14 19 4	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ$
21		eqid	$⊢ (k \in X ⟼ A) = (k \in X ⟼ A)$
22	21	fvmpts	$⊢ (j \in X \land ⦋ j / k ⦌ A \in ℝ) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
23	8 20 22	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
24		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
25	24 12	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℝ$
26	10 25	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ)$
27		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
28	27	eleq1d	$⊢ k = j \to (B \in ℝ \leftrightarrow ⦋ j / k ⦌ B \in ℝ)$
29	16 28	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to B \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ))$
30	26 29 5	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ$
31		eqid	$⊢ (k \in X ⟼ B) = (k \in X ⟼ B)$
32	31	fvmpts	$⊢ (j \in X \land ⦋ j / k ⦌ B \in ℝ) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
33	8 30 32	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
34	23 33	oveq12d	$⊢ (φ \land j \in X) \to ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = (⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
35	34	ixpeq2dva	$⊢ φ \to \underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = \underset{j \in X}{⨉} (⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
36		nfcv	$⊢ \underline{Ⅎ} k (.)$
37	11 36 24	nfov	$⊢ \underline{Ⅎ} k (⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
38		nfcv	$⊢ \underline{Ⅎ} j (A, B)$
39	17	equcoms	$⊢ j = k \to A = ⦋ j / k ⦌ A$
40	39	eqcomd	$⊢ j = k \to ⦋ j / k ⦌ A = A$
41		eqidd	$⊢ j = k \to A = A$
42	40 41	eqtrd	$⊢ j = k \to ⦋ j / k ⦌ A = A$
43	27	equcoms	$⊢ j = k \to B = ⦋ j / k ⦌ B$
44	43	eqcomd	$⊢ j = k \to ⦋ j / k ⦌ B = B$
45	42 44	oveq12d	$⊢ j = k \to (⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = (A, B)$
46	37 38 45	cbvixp	$⊢ \underset{j \in X}{⨉} (⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} (A, B)$
47	46	a1i	$⊢ φ \to \underset{j \in X}{⨉} (⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} (A, B)$
48	35 47	eqtrd	$⊢ φ \to \underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = \underset{k \in X}{⨉} (A, B)$
49	7 48	eqtr4d	$⊢ φ \to I = \underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j))$
50	49	fveq2d	$⊢ φ \to voln (X) (I) = voln (X) (\underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j)))$
51	1 4 21	fmptdf	$⊢ φ \to (k \in X ⟼ A) : X ⟶ ℝ$
52	1 5 31	fmptdf	$⊢ φ \to (k \in X ⟼ B) : X ⟶ ℝ$
53		eqid	$⊢ \underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = \underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j))$
54	2 3 51 52 53	vonn0ioo	$⊢ φ \to voln (X) (\underset{j \in X}{⨉} ((k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) = \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)))$
55	23 33	oveq12d	$⊢ (φ \land j \in X) \to [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
56	55	fveq2d	$⊢ (φ \land j \in X) \to vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) = vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
57	20 30	voliooico	$⊢ (φ \land j \in X) \to vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B)) = vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
58	57	eqcomd	$⊢ (φ \land j \in X) \to vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B)) = vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
59	56 58	eqtrd	$⊢ (φ \land j \in X) \to vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) = vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
60	59	prodeq2dv	$⊢ φ \to \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) = \prod_{j \in X} vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
61	45	fveq2d	$⊢ j = k \to vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B)) = vol ((A, B))$
62		nfcv	$⊢ \underline{Ⅎ} k X$
63		nfcv	$⊢ \underline{Ⅎ} j X$
64		nfcv	$⊢ \underline{Ⅎ} k vol$
65	64 37	nffv	$⊢ \underline{Ⅎ} k vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B))$
66		nfcv	$⊢ \underline{Ⅎ} j vol ((A, B))$
67	61 62 63 65 66	cbvprod	$⊢ \prod_{j \in X} vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B)) = \prod_{k \in X} vol ((A, B))$
68	67	a1i	$⊢ φ \to \prod_{j \in X} vol ((⦋ j / k ⦌ A, ⦋ j / k ⦌ B)) = \prod_{k \in X} vol ((A, B))$
69	60 68	eqtrd	$⊢ φ \to \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) = \prod_{k \in X} vol ((A, B))$
70	50 54 69	3eqtrd	$⊢ φ \to voln (X) (I) = \prod_{k \in X} vol ((A, B))$

Metamath Proof Explorer

Theorem vonn0ioo2

Proof