vonn0icc2

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

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

Proof

Step	Hyp	Ref	Expression
1		vonn0icc2.k	$⊢ Ⅎ k φ$
2		vonn0icc2.x	$⊢ φ \to X \in Fin$
3		vonn0icc2.n	$⊢ φ \to X \neq \emptyset$
4		vonn0icc2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
5		vonn0icc2.b	$⊢ (φ \land k \in X) \to B \in ℝ$
6		vonn0icc2.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	vonn0icc	$⊢ φ \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	34	fveq2d	$⊢ (φ \land j \in X) \to vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)]) = vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B])$
56	55	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])$
57	45	fveq2d	$⊢ j = k \to vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B]) = vol ([A, B])$
58		nfcv	$⊢ \underline{Ⅎ} k X$
59		nfcv	$⊢ \underline{Ⅎ} j X$
60		nfcv	$⊢ \underline{Ⅎ} k vol$
61	60 37	nffv	$⊢ \underline{Ⅎ} k vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B])$
62		nfcv	$⊢ \underline{Ⅎ} j vol ([A, B])$
63	57 58 59 61 62	cbvprod	$⊢ \prod_{j \in X} vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B]) = \prod_{k \in X} vol ([A, B])$
64	63	a1i	$⊢ φ \to \prod_{j \in X} vol ([⦋ j / k ⦌ A, ⦋ j / k ⦌ B]) = \prod_{k \in X} vol ([A, B])$
65	56 64	eqtrd	$⊢ φ \to \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)]) = \prod_{k \in X} vol ([A, B])$
66	50 54 65	3eqtrd	$⊢ φ \to voln (X) (I) = \prod_{k \in X} vol ([A, B])$

Metamath Proof Explorer

Theorem vonn0icc2

Proof