vonhoire

Description: The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonhoire.n	$⊢ Ⅎ k φ$
	vonhoire.x	$⊢ φ \to X \in Fin$
	vonhoire.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	vonhoire.b	$⊢ (φ \land k \in X) \to B \in ℝ$
Assertion	vonhoire	$⊢ φ \to voln (X) (\underset{k \in X}{⨉} [A, B)) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		vonhoire.n	$⊢ Ⅎ k φ$
2		vonhoire.x	$⊢ φ \to X \in Fin$
3		vonhoire.a	$⊢ (φ \land k \in X) \to A \in ℝ$
4		vonhoire.b	$⊢ (φ \land k \in X) \to B \in ℝ$
5		fveq2	$⊢ X = \emptyset \to voln (X) = voln (\emptyset)$
6	5	fveq1d	$⊢ X = \emptyset \to voln (X) (\underset{k \in X}{⨉} [A, B)) = voln (\emptyset) (\underset{k \in X}{⨉} [A, B))$
7	6	adantl	$⊢ (φ \land X = \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) = voln (\emptyset) (\underset{k \in X}{⨉} [A, B))$
8		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A, B) = \underset{k \in \emptyset}{⨉} [A, B)$
9	8	adantl	$⊢ (φ \land X = \emptyset) \to \underset{k \in X}{⨉} [A, B) = \underset{k \in \emptyset}{⨉} [A, B)$
10		0fi	$⊢ \emptyset \in Fin$
11	10	a1i	$⊢ φ \to \emptyset \in Fin$
12		eqid	$⊢ dom voln (\emptyset) = dom voln (\emptyset)$
13		noel	$⊢ \neg k \in \emptyset$
14	13	pm2.21i	$⊢ k \in \emptyset \to A \in ℝ$
15	14	adantl	$⊢ (φ \land k \in \emptyset) \to A \in ℝ$
16	13	pm2.21i	$⊢ k \in \emptyset \to B \in ℝ$
17	16	adantl	$⊢ (φ \land k \in \emptyset) \to B \in ℝ$
18	1 11 12 15 17	hoimbl2	$⊢ φ \to \underset{k \in \emptyset}{⨉} [A, B) \in dom voln (\emptyset)$
19	18	adantr	$⊢ (φ \land X = \emptyset) \to \underset{k \in \emptyset}{⨉} [A, B) \in dom voln (\emptyset)$
20	9 19	eqeltrd	$⊢ (φ \land X = \emptyset) \to \underset{k \in X}{⨉} [A, B) \in dom voln (\emptyset)$
21	20	von0val	$⊢ (φ \land X = \emptyset) \to voln (\emptyset) (\underset{k \in X}{⨉} [A, B)) = 0$
22	7 21	eqtrd	$⊢ (φ \land X = \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) = 0$
23		0red	$⊢ (φ \land X = \emptyset) \to 0 \in ℝ$
24	22 23	eqeltrd	$⊢ (φ \land X = \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) \in ℝ$
25		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
26	25	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
27		simpr	$⊢ (φ \land j \in X) \to j \in X$
28		nfv	$⊢ Ⅎ k j \in X$
29	1 28	nfan	$⊢ Ⅎ k (φ \land j \in X)$
30		nfcv	$⊢ \underline{Ⅎ} k j$
31	30	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
32	31	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ A \in ℝ$
33	29 32	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ)$
34		eleq1w	$⊢ k = j \to (k \in X \leftrightarrow j \in X)$
35	34	anbi2d	$⊢ k = j \to ((φ \land k \in X) \leftrightarrow (φ \land j \in X))$
36		csbeq1a	$⊢ k = j \to A = ⦋ j / k ⦌ A$
37	36	eleq1d	$⊢ k = j \to (A \in ℝ \leftrightarrow ⦋ j / k ⦌ A \in ℝ)$
38	35 37	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to A \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ))$
39	33 38 3	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ$
40		eqid	$⊢ (k \in X ⟼ A) = (k \in X ⟼ A)$
41	30 31 36 40	fvmptf	$⊢ (j \in X \land ⦋ j / k ⦌ A \in ℝ) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
42	27 39 41	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
43	30	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
44		nfcv	$⊢ \underline{Ⅎ} k ℝ$
45	43 44	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℝ$
46	29 45	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ)$
47		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
48	47	eleq1d	$⊢ k = j \to (B \in ℝ \leftrightarrow ⦋ j / k ⦌ B \in ℝ)$
49	35 48	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to B \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ))$
50	46 49 4	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ$
51		eqid	$⊢ (k \in X ⟼ B) = (k \in X ⟼ B)$
52	30 43 47 51	fvmptf	$⊢ (j \in X \land ⦋ j / k ⦌ B \in ℝ) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
53	27 50 52	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
54	42 53	oveq12d	$⊢ (φ \land j \in X) \to [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
55	54	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)$
56		nfcv	$⊢ \underline{Ⅎ} j [A, B)$
57		nfcv	$⊢ \underline{Ⅎ} k [.)$
58	31 57 43	nfov	$⊢ \underline{Ⅎ} k [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
59	36 47	oveq12d	$⊢ k = j \to [A, B) = [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
60	56 58 59	cbvixp	$⊢ \underset{k \in X}{⨉} [A, B) = \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
61	60	eqcomi	$⊢ \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} [A, B)$
62	61	a1i	$⊢ φ \to \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} [A, B)$
63	55 62	eqtr2d	$⊢ φ \to \underset{k \in X}{⨉} [A, B) = \underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))$
64	63	fveq2d	$⊢ φ \to voln (X) (\underset{k \in X}{⨉} [A, B)) = voln (X) (\underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)))$
65	64	adantr	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) = voln (X) (\underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)))$
66	2	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
67		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
68	1 3 40	fmptdf	$⊢ φ \to (k \in X ⟼ A) : X ⟶ ℝ$
69	68	adantr	$⊢ (φ \land X \neq \emptyset) \to (k \in X ⟼ A) : X ⟶ ℝ$
70	1 4 51	fmptdf	$⊢ φ \to (k \in X ⟼ B) : X ⟶ ℝ$
71	70	adantr	$⊢ (φ \land X \neq \emptyset) \to (k \in X ⟼ B) : X ⟶ ℝ$
72		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))$
73	66 67 69 71 72	vonn0hoi	$⊢ (φ \land X \neq \emptyset) \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)))$
74	65 73	eqtrd	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) = \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)))$
75	42 39	eqeltrd	$⊢ (φ \land j \in X) \to (k \in X ⟼ A) (j) \in ℝ$
76	53 50	eqeltrd	$⊢ (φ \land j \in X) \to (k \in X ⟼ B) (j) \in ℝ$
77		volicore	$⊢ ((k \in X ⟼ A) (j) \in ℝ \land (k \in X ⟼ B) (j) \in ℝ) \to vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) \in ℝ$
78	75 76 77	syl2anc	$⊢ (φ \land j \in X) \to vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) \in ℝ$
79	2 78	fprodrecl	$⊢ φ \to \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) \in ℝ$
80	79	adantr	$⊢ (φ \land X \neq \emptyset) \to \prod_{j \in X} vol ([(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))) \in ℝ$
81	74 80	eqeltrd	$⊢ (φ \land X \neq \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) \in ℝ$
82	26 81	syldan	$⊢ (φ \land \neg X = \emptyset) \to voln (X) (\underset{k \in X}{⨉} [A, B)) \in ℝ$
83	24 82	pm2.61dan	$⊢ φ \to voln (X) (\underset{k \in X}{⨉} [A, B)) \in ℝ$

Metamath Proof Explorer

Theorem vonhoire

Proof