Theorem 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	⊢ Ⅎ 𝑘 𝜑
	vonn0ioo2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonn0ioo2.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	vonn0ioo2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
	vonn0ioo2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
	vonn0ioo2.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 )
Assertion	vonn0ioo2	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonn0ioo2.k	⊢ Ⅎ 𝑘 𝜑
2		vonn0ioo2.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		vonn0ioo2.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4		vonn0ioo2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
5		vonn0ioo2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
6		vonn0ioo2.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 )
7	6	a1i	⊢ ( 𝜑 → 𝐼 = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑗 ∈ 𝑋 )
9		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑋
10	1 9	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑋 )
11		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
12		nfcv	⊢ Ⅎ 𝑘 ℝ
13	11 12	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ
14	10 13	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
15		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑋 ↔ 𝑗 ∈ 𝑋 ) )
16	15	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ) )
17		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
18	17	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) )
19	16 18	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) ) )
20	14 19 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
21		eqid	⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐴 )
22	21	fvmpts	⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
23	8 20 22	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
24		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
25	24 12	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ
26	10 25	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
27		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
28	27	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
29	16 28	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
30	26 29 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
31		eqid	⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐵 )
32	31	fvmpts	⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
33	8 30 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
34	23 33	oveq12d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
35	34	ixpeq2dva	⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
36		nfcv	⊢ Ⅎ 𝑘 (,)
37	11 36 24	nfov	⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
38		nfcv	⊢ Ⅎ 𝑗 ( 𝐴 (,) 𝐵 )
39	17	equcoms	⊢ ( 𝑗 = 𝑘 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
40	39	eqcomd	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 = 𝐴 )
41		eqidd	⊢ ( 𝑗 = 𝑘 → 𝐴 = 𝐴 )
42	40 41	eqtrd	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 = 𝐴 )
43	27	equcoms	⊢ ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
44	43	eqcomd	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 𝐵 )
45	42 44	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = ( 𝐴 (,) 𝐵 ) )
46	37 38 45	cbvixp	⊢ X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 )
47	46	a1i	⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
48	35 47	eqtrd	⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
49	7 48	eqtr4d	⊢ ( 𝜑 → 𝐼 = X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) )
50	49	fveq2d	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln ‘ 𝑋 ) ‘ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
51	1 4 21	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℝ )
52	1 5 31	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
53		eqid	⊢ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) )
54	2 3 51 52 53	vonn0ioo	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) (,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) )
55	23 33	oveq12d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
56	55	fveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
57	20 30	voliooico	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) = ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
58	57	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) = ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
59	56 58	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
60	59	prodeq2dv	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
61	45	fveq2d	⊢ ( 𝑗 = 𝑘 → ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
62		nfcv	⊢ Ⅎ 𝑘 𝑋
63		nfcv	⊢ Ⅎ 𝑗 𝑋
64		nfcv	⊢ Ⅎ 𝑘 vol
65	64 37	nffv	⊢ Ⅎ 𝑘 ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
66		nfcv	⊢ Ⅎ 𝑗 ( vol ‘ ( 𝐴 (,) 𝐵 ) )
67	61 62 63 65 66	cbvprod	⊢ ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 (,) 𝐵 ) )
68	67	a1i	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 (,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
69	60 68	eqtrd	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝑋 ( vol ‘ ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
70	50 54 69	3eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )