hspmbllem3

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hspmbllem3.h	⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
	hspmbllem3.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hspmbllem3.i	⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
	hspmbllem3.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	hspmbllem3.a	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
	hspmbllem3.s	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
	hspmbllem3.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
	hspmbllem3.l	⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
	hspmbllem3.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑟 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) )
	hspmbllem3.10	⊢ 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
	hspmbllem3.11	⊢ 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
Assertion	hspmbllem3	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +_e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hspmbllem3.h	⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
2		hspmbllem3.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hspmbllem3.i	⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
4		hspmbllem3.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5		hspmbllem3.a	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
6		hspmbllem3.s	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
7		hspmbllem3.c	⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } )
8		hspmbllem3.l	⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) )
9		hspmbllem3.d	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑟 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) )
10		hspmbllem3.10	⊢ 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 1^st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
11		hspmbllem3.11	⊢ 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 2^nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) )
12		inss1	⊢ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ 𝐴
13	12 6	sstrid	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑_m 𝑋 ) )
14	2 13	ovncl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ( 0 [,] +∞ ) )
15	12	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ 𝐴 )
16	2 15 6	ovnssle	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
17	5 14 16	ge0lere	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
18	6	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ ( ℝ ↑_m 𝑋 ) )
19	2 18	ovncl	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ( 0 [,] +∞ ) )
20		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ⊆ 𝐴 )
21	2 20 6	ovnssle	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
22	5 19 21	ge0lere	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
23		rexadd	⊢ ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ ∧ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +_e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) )
24	17 22 23	syl2anc	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +_e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) )
25	2	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → 𝑋 ∈ Fin )
26	3	ne0d	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → 𝑋 ≠ ∅ )
28	6	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
29		simpr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → 𝑒 ∈ ℝ⁺ )
30	25 27 28 29 7 8 9	ovncvrrp	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) )
31	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑋 ∈ Fin )
32	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐾 ∈ 𝑋 )
33	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑌 ∈ ℝ )
34	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑒 ∈ ℝ⁺ )
35	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
36		fveq1	⊢ ( 𝑖 = ℎ → ( 𝑖 ‘ 𝑗 ) = ( ℎ ‘ 𝑗 ) )
37	36	fveq2d	⊢ ( 𝑖 = ℎ → ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) = ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) )
38	37	mpteq2dv	⊢ ( 𝑖 = ℎ → ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) )
39	38	fveq2d	⊢ ( 𝑖 = ℎ → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
40	39	breq1d	⊢ ( 𝑖 = ℎ → ( ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) ↔ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) ) )
41	40	cbvrabv	⊢ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } = { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) }
42	41	mpteq2i	⊢ ( 𝑟 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) = ( 𝑟 ∈ ℝ⁺ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } )
43	42	mpteq2i	⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑟 ∈ ℝ⁺ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑟 ∈ ℝ⁺ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) )
44	9 43	eqtri	⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ ( 𝑟 ∈ ℝ⁺ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +_e 𝑟 ) } ) )
45		simpr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) )
46	31 35 34 7 8 44 45 10 11	ovncvr2	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( ( 𝐵 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +_e 𝑒 ) ) )
47	46	simplld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( 𝐵 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) ) )
48	47	simpld	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐵 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
49	47	simprd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑇 : ℕ ⟶ ( ℝ ↑_m 𝑋 ) )
50	46	simplrd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) )
51	46	simprd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +_e 𝑒 ) )
52	5	adantr	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
53	29	rpred	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → 𝑒 ∈ ℝ )
54	52 53	rexaddd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +_e 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
55	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +_e 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
56	51 55	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
57	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ )
58	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
59	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ∈ ℝ )
60		eqid	⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑_m 𝑥 ) , 𝑏 ∈ ( ℝ ↑_m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑_m 𝑥 ) , 𝑏 ∈ ( ℝ ↑_m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
61		eqid	⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑_m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑_m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ ∈ ( 𝑋 ∖ { 𝐾 } ) , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑦 , ( 𝑐 ‘ ℎ ) , 𝑦 ) ) ) ) )
62		eqid	⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑_m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ‘ ℎ ) , ( 𝑐 ‘ ℎ ) , 𝑥 ) , ( 𝑐 ‘ ℎ ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑_m 𝑋 ) ↦ ( ℎ ∈ 𝑋 ↦ if ( ℎ = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ‘ ℎ ) , ( 𝑐 ‘ ℎ ) , 𝑥 ) , ( 𝑐 ‘ ℎ ) ) ) ) )
63	1 31 32 33 34 48 49 50 56 57 58 59 60 61 62	hspmbllem2	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
64	63	ex	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ( 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
65	64	exlimdv	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ( ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
66	30 65	mpd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ⁺ ) → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
67	66	ralrimiva	⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ⁺ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) )
68	17 22	readdcld	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ∈ ℝ )
69		alrple	⊢ ( ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ∈ ℝ ∧ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ ) → ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ⁺ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
70	68 5 69	syl2anc	⊢ ( 𝜑 → ( ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ↔ ∀ 𝑒 ∈ ℝ⁺ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) )
71	67 70	mpbird	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
72	24 71	eqbrtrd	⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +_e ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem hspmbllem3

Proof