hspmbl

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hspmbl.1	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
	hspmbl.x	$⊢ φ \to X \in Fin$
	hspmbl.i	$⊢ φ \to K \in X$
	hspmbl.y	$⊢ φ \to Y \in ℝ$
Assertion	hspmbl	$⊢ φ \to K H (X) Y \in dom voln (X)$

Proof

Step	Hyp	Ref	Expression
1		hspmbl.1	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
2		hspmbl.x	$⊢ φ \to X \in Fin$
3		hspmbl.i	$⊢ φ \to K \in X$
4		hspmbl.y	$⊢ φ \to Y \in ℝ$
5	2	ovnome	$⊢ φ \to voln* (X) \in OutMeas$
6		eqid	$⊢ ⋃ dom voln* (X) = ⋃ dom voln* (X)$
7		eqid	$⊢ CaraGen (voln* (X)) = CaraGen (voln* (X))$
8		ovex	$⊢ (−∞, Y) \in V$
9		reex	$⊢ ℝ \in V$
10	8 9	ifex	$⊢ if (p = K, (−∞, Y), ℝ) \in V$
11	10	ixpssmap	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \subseteq {⋃_{p \in X} if (p = K, (−∞, Y), ℝ)}^{X}$
12		iftrue	$⊢ p = K \to if (p = K, (−∞, Y), ℝ) = (−∞, Y)$
13		ioossre	$⊢ (−∞, Y) \subseteq ℝ$
14	13	a1i	$⊢ p = K \to (−∞, Y) \subseteq ℝ$
15	12 14	eqsstrd	$⊢ p = K \to if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
16		iffalse	$⊢ \neg p = K \to if (p = K, (−∞, Y), ℝ) = ℝ$
17		ssid	$⊢ ℝ \subseteq ℝ$
18	17	a1i	$⊢ \neg p = K \to ℝ \subseteq ℝ$
19	16 18	eqsstrd	$⊢ \neg p = K \to if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
20	15 19	pm2.61i	$⊢ if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
21	20	rgenw	$⊢ \forall p \in X if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
22		iunss	$⊢ ⋃_{p \in X} if (p = K, (−∞, Y), ℝ) \subseteq ℝ \leftrightarrow \forall p \in X if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
23	21 22	mpbir	$⊢ ⋃_{p \in X} if (p = K, (−∞, Y), ℝ) \subseteq ℝ$
24		mapss	$⊢ (ℝ \in V \land ⋃_{p \in X} if (p = K, (−∞, Y), ℝ) \subseteq ℝ) \to {⋃_{p \in X} if (p = K, (−∞, Y), ℝ)}^{X} \subseteq ℝ^{X}$
25	9 23 24	mp2an	$⊢ {⋃_{p \in X} if (p = K, (−∞, Y), ℝ)}^{X} \subseteq ℝ^{X}$
26	11 25	sstri	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \subseteq ℝ^{X}$
27	10	rgenw	$⊢ \forall p \in X if (p = K, (−∞, Y), ℝ) \in V$
28		ixpexg	$⊢ \forall p \in X if (p = K, (−∞, Y), ℝ) \in V \to \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in V$
29	27 28	ax-mp	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in V$
30		elpwg	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in V \to (\underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in 𝒫 (ℝ^{X}) \leftrightarrow \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \subseteq ℝ^{X})$
31	29 30	ax-mp	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in 𝒫 (ℝ^{X}) \leftrightarrow \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \subseteq ℝ^{X}$
32	26 31	mpbir	$⊢ \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in 𝒫 (ℝ^{X})$
33	32	a1i	$⊢ φ \to \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in 𝒫 (ℝ^{X})$
34		equid	$⊢ x = x$
35		eqid	$⊢ ℝ = ℝ$
36		equequ1	$⊢ k = p \to (k = l \leftrightarrow p = l)$
37	36	ifbid	$⊢ k = p \to if (k = l, (−∞, y), ℝ) = if (p = l, (−∞, y), ℝ)$
38	37	cbvixpv	$⊢ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ) = \underset{p \in x}{⨉} if (p = l, (−∞, y), ℝ)$
39	34 35 38	mpoeq123i	$⊢ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)) = (l \in x, y \in ℝ ⟼ \underset{p \in x}{⨉} if (p = l, (−∞, y), ℝ))$
40	39	mpteq2i	$⊢ (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ))) = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{p \in x}{⨉} if (p = l, (−∞, y), ℝ)))$
41	1 40	eqtri	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{p \in x}{⨉} if (p = l, (−∞, y), ℝ)))$
42	41 2 3 4	hspval	$⊢ φ \to K H (X) Y = \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ)$
43	2	ovnf	$⊢ φ \to voln* (X) : 𝒫 (ℝ^{X}) ⟶ [0, +∞]$
44	43	fdmd	$⊢ φ \to dom voln* (X) = 𝒫 (ℝ^{X})$
45	44	unieqd	$⊢ φ \to ⋃ dom voln* (X) = ⋃ 𝒫 (ℝ^{X})$
46		unipw	$⊢ ⋃ 𝒫 (ℝ^{X}) = ℝ^{X}$
47	46	a1i	$⊢ φ \to ⋃ 𝒫 (ℝ^{X}) = ℝ^{X}$
48	45 47	eqtrd	$⊢ φ \to ⋃ dom voln* (X) = ℝ^{X}$
49	48	pweqd	$⊢ φ \to 𝒫 ⋃ dom voln* (X) = 𝒫 (ℝ^{X})$
50	42 49	eleq12d	$⊢ φ \to (K H (X) Y \in 𝒫 ⋃ dom voln* (X) \leftrightarrow \underset{p \in X}{⨉} if (p = K, (−∞, Y), ℝ) \in 𝒫 (ℝ^{X}))$
51	33 50	mpbird	$⊢ φ \to K H (X) Y \in 𝒫 ⋃ dom voln* (X)$
52		simpl	$⊢ (φ \land a \in 𝒫 ⋃ dom voln* (X)) \to φ$
53		simpr	$⊢ (φ \land a \in 𝒫 ⋃ dom voln* (X)) \to a \in 𝒫 ⋃ dom voln* (X)$
54	52 49	syl	$⊢ (φ \land a \in 𝒫 ⋃ dom voln* (X)) \to 𝒫 ⋃ dom voln* (X) = 𝒫 (ℝ^{X})$
55	53 54	eleqtrd	$⊢ (φ \land a \in 𝒫 ⋃ dom voln* (X)) \to a \in 𝒫 (ℝ^{X})$
56	2	adantr	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to X \in Fin$
57		inss1	$⊢ a \cap (K H (X) Y) \subseteq a$
58	57	a1i	$⊢ a \in 𝒫 (ℝ^{X}) \to a \cap (K H (X) Y) \subseteq a$
59		elpwi	$⊢ a \in 𝒫 (ℝ^{X}) \to a \subseteq ℝ^{X}$
60	58 59	sstrd	$⊢ a \in 𝒫 (ℝ^{X}) \to a \cap (K H (X) Y) \subseteq ℝ^{X}$
61	60	adantl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to a \cap (K H (X) Y) \subseteq ℝ^{X}$
62	56 61	ovnxrcl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a \cap (K H (X) Y)) \in ℝ^{*}$
63	59	adantl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to a \subseteq ℝ^{X}$
64	63	ssdifssd	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to a ∖ (K H (X) Y) \subseteq ℝ^{X}$
65	56 64	ovnxrcl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a ∖ (K H (X) Y)) \in ℝ^{*}$
66	62 65	xaddcld	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \in ℝ^{*}$
67		pnfge	$⊢ voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \in ℝ^{} \to voln (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq +∞$
68	66 67	syl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq +∞$
69	68	adantr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) = +∞) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq +∞$
70		id	$⊢ voln* (X) (a) = +∞ \to voln* (X) (a) = +∞$
71	70	eqcomd	$⊢ voln* (X) (a) = +∞ \to +∞ = voln* (X) (a)$
72	71	adantl	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) = +∞) \to +∞ = voln* (X) (a)$
73	69 72	breqtrd	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) = +∞) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq voln* (X) (a)$
74		simpl	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land \neg voln* (X) (a) = +∞) \to (φ \land a \in 𝒫 (ℝ^{X}))$
75	56 63	ovncl	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a) \in [0, +∞]$
76	75	adantr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land \neg voln* (X) (a) = +∞) \to voln* (X) (a) \in [0, +∞]$
77		neqne	$⊢ \neg voln* (X) (a) = +∞ \to voln* (X) (a) \neq +∞$
78	77	adantl	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land \neg voln* (X) (a) = +∞) \to voln* (X) (a) \neq +∞$
79		ge0xrre	$⊢ (voln* (X) (a) \in [0, +∞] \land voln* (X) (a) \neq +∞) \to voln* (X) (a) \in ℝ$
80	76 78 79	syl2anc	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land \neg voln* (X) (a) = +∞) \to voln* (X) (a) \in ℝ$
81	56	adantr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to X \in Fin$
82	3	ad2antrr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to K \in X$
83	4	ad2antrr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to Y \in ℝ$
84		simpr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to voln* (X) (a) \in ℝ$
85	63	adantr	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to a \subseteq ℝ^{X}$
86		sseq1	$⊢ a = b \to (a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p) \leftrightarrow b \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p))$
87	86	rabbidv	$⊢ a = b \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}$
88	87	cbvmptv	$⊢ (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) = (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\})$
89		simpl	$⊢ (i = h \land p \in X) \to i = h$
90	89	coeq2d	$⊢ (i = h \land p \in X) \to [.) \circ i = [.) \circ h$
91	90	fveq1d	$⊢ (i = h \land p \in X) \to ([.) \circ i) (p) = ([.) \circ h) (p)$
92	91	fveq2d	$⊢ (i = h \land p \in X) \to vol (([.) \circ i) (p)) = vol (([.) \circ h) (p))$
93	92	prodeq2dv	$⊢ i = h \to \prod_{p \in X} vol (([.) \circ i) (p)) = \prod_{p \in X} vol (([.) \circ h) (p))$
94	93	cbvmptv	$⊢ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ h) (p)))$
95		fveq2	$⊢ n = p \to ([.) \circ m (i)) (n) = ([.) \circ m (i)) (p)$
96	95	cbvixpv	$⊢ \underset{n \in X}{⨉} ([.) \circ m (i)) (n) = \underset{p \in X}{⨉} ([.) \circ m (i)) (p)$
97	96	a1i	$⊢ m = h \to \underset{n \in X}{⨉} ([.) \circ m (i)) (n) = \underset{p \in X}{⨉} ([.) \circ m (i)) (p)$
98		fveq1	$⊢ m = h \to m (i) = h (i)$
99	98	coeq2d	$⊢ m = h \to [.) \circ m (i) = [.) \circ h (i)$
100	99	fveq1d	$⊢ m = h \to ([.) \circ m (i)) (p) = ([.) \circ h (i)) (p)$
101	100	ixpeq2dv	$⊢ m = h \to \underset{p \in X}{⨉} ([.) \circ m (i)) (p) = \underset{p \in X}{⨉} ([.) \circ h (i)) (p)$
102	97 101	eqtrd	$⊢ m = h \to \underset{n \in X}{⨉} ([.) \circ m (i)) (n) = \underset{p \in X}{⨉} ([.) \circ h (i)) (p)$
103	102	adantr	$⊢ (m = h \land i \in ℕ) \to \underset{n \in X}{⨉} ([.) \circ m (i)) (n) = \underset{p \in X}{⨉} ([.) \circ h (i)) (p)$
104	103	iuneq2dv	$⊢ m = h \to ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n) = ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p)$
105	104	sseq2d	$⊢ m = h \to (a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n) \leftrightarrow a \subseteq ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p))$
106	105	cbvrabv	$⊢ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\} = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p)\}$
107		fveq1	$⊢ h = l \to h (i) = l (i)$
108	107	coeq2d	$⊢ h = l \to [.) \circ h (i) = [.) \circ l (i)$
109	108	fveq1d	$⊢ h = l \to ([.) \circ h (i)) (p) = ([.) \circ l (i)) (p)$
110	109	ixpeq2dv	$⊢ h = l \to \underset{p \in X}{⨉} ([.) \circ h (i)) (p) = \underset{p \in X}{⨉} ([.) \circ l (i)) (p)$
111	110	adantr	$⊢ (h = l \land i \in ℕ) \to \underset{p \in X}{⨉} ([.) \circ h (i)) (p) = \underset{p \in X}{⨉} ([.) \circ l (i)) (p)$
112	111	iuneq2dv	$⊢ h = l \to ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p) = ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (i)) (p)$
113		fveq2	$⊢ i = j \to l (i) = l (j)$
114	113	coeq2d	$⊢ i = j \to [.) \circ l (i) = [.) \circ l (j)$
115	114	fveq1d	$⊢ i = j \to ([.) \circ l (i)) (p) = ([.) \circ l (j)) (p)$
116	115	ixpeq2dv	$⊢ i = j \to \underset{p \in X}{⨉} ([.) \circ l (i)) (p) = \underset{p \in X}{⨉} ([.) \circ l (j)) (p)$
117	116	cbviunv	$⊢ ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (i)) (p) = ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)$
118	117	a1i	$⊢ h = l \to ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (i)) (p) = ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)$
119	112 118	eqtrd	$⊢ h = l \to ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p) = ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)$
120	119	sseq2d	$⊢ h = l \to (a \subseteq ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p) \leftrightarrow a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p))$
121	120	cbvrabv	$⊢ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{p \in X}{⨉} ([.) \circ h (i)) (p)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}$
122	106 121	eqtri	$⊢ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}$
123	122	mpteq2i	$⊢ (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\})$
124	123	a1i	$⊢ c = b \to (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\})$
125		id	$⊢ c = b \to c = b$
126	124 125	fveq12d	$⊢ c = b \to (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b)$
127	126	eleq2d	$⊢ c = b \to (t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \leftrightarrow t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b))$
128		2fveq3	$⊢ m = p \to vol (([.) \circ i) (m)) = vol (([.) \circ i) (p))$
129	128	cbvprodv	$⊢ \prod_{m \in X} vol (([.) \circ i) (m)) = \prod_{p \in X} vol (([.) \circ i) (p))$
130	129	mpteq2i	$⊢ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p)))$
131	130	a1i	$⊢ m = j \to (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p)))$
132		fveq2	$⊢ m = j \to t (m) = t (j)$
133	131 132	fveq12d	$⊢ m = j \to (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)) = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j))$
134	133	cbvmptv	$⊢ (m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m))) = (j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))$
135	134	a1i	$⊢ c = b \to (m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m))) = (j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))$
136	135	fveq2d	$⊢ c = b \to sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) = sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j))))$
137		fveq2	$⊢ c = b \to voln* (X) (c) = voln* (X) (b)$
138	137	oveq1d	$⊢ c = b \to voln* (X) (c) +_{𝑒} s = voln* (X) (b) +_{𝑒} s$
139	136 138	breq12d	$⊢ c = b \to (sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s \leftrightarrow sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s)$
140	127 139	anbi12d	$⊢ c = b \to ((t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \land sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s) \leftrightarrow (t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \land sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s))$
141	140	rabbidva2	$⊢ c = b \to \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \| sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s\} = \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s\}$
142	141	mpteq2dv	$⊢ c = b \to (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \| sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s\}) = (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s\})$
143		eqidd	$⊢ s = r \to (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b)$
144	143	eleq2d	$⊢ s = r \to (t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \leftrightarrow t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b))$
145		oveq2	$⊢ s = r \to voln* (X) (b) +_{𝑒} s = voln* (X) (b) +_{𝑒} r$
146	145	breq2d	$⊢ s = r \to (sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s \leftrightarrow sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r)$
147	144 146	anbi12d	$⊢ s = r \to ((t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \land sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s) \leftrightarrow (t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \land sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r))$
148	147	rabbidva2	$⊢ s = r \to \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s\} = \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r\}$
149	148	cbvmptv	$⊢ (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s\}) = (r \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r\})$
150	149	a1i	$⊢ c = b \to (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} s\}) = (r \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r\})$
151	142 150	eqtrd	$⊢ c = b \to (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \| sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s\}) = (r \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r\})$
152	151	cbvmptv	$⊢ (c \in 𝒫 (ℝ^{X}) ⟼ (s \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{m \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{i \in ℕ} \underset{n \in X}{⨉} ([.) \circ m (i)) (n)\}) (c) \| sum^((m \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{m \in X} vol (([.) \circ i) (m))) (t (m)))) \leq voln* (X) (c) +_{𝑒} s\})) = (b \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{t \in (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{p \in X}{⨉} ([.) \circ l (j)) (p)\}) (b) \| sum^((j \in ℕ ⟼ (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{p \in X} vol (([.) \circ i) (p))) (t (j)))) \leq voln* (X) (b) +_{𝑒} r\}))$
153		2fveq3	$⊢ m = p \to 1^{st} (t (j) (m)) = 1^{st} (t (j) (p))$
154	153	cbvmptv	$⊢ (m \in X ⟼ 1^{st} (t (j) (m))) = (p \in X ⟼ 1^{st} (t (j) (p)))$
155	154	mpteq2i	$⊢ (j \in ℕ ⟼ (m \in X ⟼ 1^{st} (t (j) (m)))) = (j \in ℕ ⟼ (p \in X ⟼ 1^{st} (t (j) (p))))$
156		fveq2	$⊢ i = j \to t (i) = t (j)$
157	156	fveq1d	$⊢ i = j \to t (i) (m) = t (j) (m)$
158	157	fveq2d	$⊢ i = j \to 2^{nd} (t (i) (m)) = 2^{nd} (t (j) (m))$
159	158	mpteq2dv	$⊢ i = j \to (m \in X ⟼ 2^{nd} (t (i) (m))) = (m \in X ⟼ 2^{nd} (t (j) (m)))$
160		2fveq3	$⊢ m = p \to 2^{nd} (t (j) (m)) = 2^{nd} (t (j) (p))$
161	160	cbvmptv	$⊢ (m \in X ⟼ 2^{nd} (t (j) (m))) = (p \in X ⟼ 2^{nd} (t (j) (p)))$
162	161	a1i	$⊢ i = j \to (m \in X ⟼ 2^{nd} (t (j) (m))) = (p \in X ⟼ 2^{nd} (t (j) (p)))$
163	159 162	eqtrd	$⊢ i = j \to (m \in X ⟼ 2^{nd} (t (i) (m))) = (p \in X ⟼ 2^{nd} (t (j) (p)))$
164	163	cbvmptv	$⊢ (i \in ℕ ⟼ (m \in X ⟼ 2^{nd} (t (i) (m)))) = (j \in ℕ ⟼ (p \in X ⟼ 2^{nd} (t (j) (p))))$
165	41 81 82 83 84 85 88 94 152 155 164	hspmbllem3	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land voln* (X) (a) \in ℝ) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq voln* (X) (a)$
166	74 80 165	syl2anc	$⊢ ((φ \land a \in 𝒫 (ℝ^{X})) \land \neg voln* (X) (a) = +∞) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq voln* (X) (a)$
167	73 166	pm2.61dan	$⊢ (φ \land a \in 𝒫 (ℝ^{X})) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq voln* (X) (a)$
168	52 55 167	syl2anc	$⊢ (φ \land a \in 𝒫 ⋃ dom voln* (X)) \to voln* (X) (a \cap (K H (X) Y)) +_{𝑒} voln* (X) (a ∖ (K H (X) Y)) \leq voln* (X) (a)$
169	5 6 7 51 168	caragenel2d	$⊢ φ \to K H (X) Y \in CaraGen (voln* (X))$
170	2	dmvon	$⊢ φ \to dom voln (X) = CaraGen (voln* (X))$
171	170	eqcomd	$⊢ φ \to CaraGen (voln* (X)) = dom voln (X)$
172	169 171	eleqtrd	$⊢ φ \to K H (X) Y \in dom voln (X)$

Metamath Proof Explorer

Theorem hspmbl

Proof