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 = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoiprodp1.y	$⊢ φ \to Y \in Fin$
	hoiprodp1.3	$⊢ φ \to Z \in V$
	hoiprodp1.z	$⊢ φ \to \neg Z \in Y$
	hoiprodp1.x	$⊢ X = Y \cup \{Z\}$
	hoiprodp1.a	$⊢ φ \to A : X ⟶ ℝ$
	hoiprodp1.b	$⊢ φ \to B : X ⟶ ℝ$
	hoiprodp1.g	$⊢ G = \prod_{k \in Y} vol ([A (k), B (k)))$
Assertion	hoiprodp1	$⊢ φ \to A L (X) B = G vol ([A (Z), B (Z)))$

Proof

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

Metamath Proof Explorer

Theorem hoiprodp1

Proof