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* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) ) |
10 |
|
hspmbllem3.10 |
⊢ 𝐵 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 1st ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
11 |
|
hspmbllem3.11 |
⊢ 𝑇 = ( 𝑗 ∈ ℕ ↦ ( 𝑘 ∈ 𝑋 ↦ ( 2nd ‘ ( ( 𝑖 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) |
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* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) = ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) + ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ) |
24 |
17 22 23
|
syl2anc |
⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( 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* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ↔ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) ) ) |
41 |
40
|
cbvrabv |
⊢ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } = { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } |
42 |
41
|
mpteq2i |
⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) |
43 |
42
|
mpteq2i |
⊢ ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) ) = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) ) |
44 |
9 43
|
eqtri |
⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑟 ∈ ℝ+ ↦ { ℎ ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( ℎ ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑟 ) } ) ) |
45 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) |
46 |
31 35 34 7 8 44 45 10 11
|
ovncvr2 |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) ) ) |
47 |
46
|
simplld |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ∧ 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) ) |
48 |
47
|
simpld |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐵 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
49 |
47
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝑇 : ℕ ⟶ ( ℝ ↑m 𝑋 ) ) |
50 |
46
|
simplrd |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
51 |
46
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( ( 𝐵 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑇 ‘ 𝑗 ) ‘ 𝑘 ) ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) ) |
52 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ∈ ℝ ) |
53 |
29
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ ) |
54 |
52 53
|
rexaddd |
⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) + 𝑒 ) ) |
55 |
54
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑖 ∈ ( ( 𝐷 ‘ 𝐴 ) ‘ 𝑒 ) ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +𝑒 𝑒 ) = ( ( ( 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* ‘ 𝑋 ) ‘ ( 𝐴 ∩ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ∖ ( 𝐾 ( 𝐻 ‘ 𝑋 ) 𝑌 ) ) ) ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ) |