Proof of Theorem hsphoidmvle2
Step | Hyp | Ref
| Expression |
1 | | hsphoidmvle2.a |
. . . . 5
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
2 | | hsphoidmvle2.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
3 | 2 | eldifad 3878 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
4 | 1, 3 | ffvelrnd 6905 |
. . . 4
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
5 | | hsphoidmvle2.b |
. . . . . 6
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
6 | 5, 3 | ffvelrnd 6905 |
. . . . 5
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
7 | | hsphoidmvle2.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
8 | 6, 7 | ifcld 4485 |
. . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) |
9 | | volicore 43794 |
. . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) |
10 | 4, 8, 9 | syl2anc 587 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) |
11 | | hsphoidmvle2.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℝ) |
12 | 6, 11 | ifcld 4485 |
. . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) |
13 | | volicore 43794 |
. . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) |
14 | 4, 12, 13 | syl2anc 587 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) |
15 | | hsphoidmvle2.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
16 | | difssd 4047 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ⊆ 𝑋) |
17 | | ssfi 8851 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → (𝑋 ∖ {𝑍}) ∈ Fin) |
18 | 15, 16, 17 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ∈ Fin) |
19 | | eldifi 4041 |
. . . . . 6
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑋) |
20 | 19 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑋) |
21 | 1 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
22 | 5 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
23 | | volicore 43794 |
. . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
24 | 21, 22, 23 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
25 | 20, 24 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
26 | 18, 25 | fprodrecl 15515 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
27 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑘𝜑 |
28 | 20, 21 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐴‘𝑘) ∈ ℝ) |
29 | 20, 22 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈ ℝ) |
30 | 29 | rexrd 10883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈
ℝ*) |
31 | | icombl 24461 |
. . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
32 | 28, 30, 31 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
33 | | volge0 43177 |
. . . . 5
⊢ (((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol → 0 ≤
(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 0 ≤ (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
35 | 27, 18, 25, 34 | fprodge0 15555 |
. . 3
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
36 | 8 | rexrd 10883 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈
ℝ*) |
37 | | icombl 24461 |
. . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) |
38 | 4, 36, 37 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) |
39 | 12 | rexrd 10883 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈
ℝ*) |
40 | | icombl 24461 |
. . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) |
41 | 4, 39, 40 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) |
42 | 4 | rexrd 10883 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) |
43 | 4 | leidd 11398 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ≤ (𝐴‘𝑍)) |
44 | 6 | leidd 11398 |
. . . . . . . 8
⊢ (𝜑 → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) |
45 | 44 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) |
46 | | iftrue 4445 |
. . . . . . . . 9
⊢ ((𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) |
47 | 46 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) |
48 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) |
49 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) |
50 | 11 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐷 ∈ ℝ) |
51 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐶) |
52 | | hsphoidmvle2.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ≤ 𝐷) |
53 | 52 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ 𝐷) |
54 | 48, 49, 50, 51, 53 | letrd 10989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐷) |
55 | 54 | iftrued 4447 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) |
56 | 47, 55 | breq12d 5066 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ (𝐵‘𝑍) ≤ (𝐵‘𝑍))) |
57 | 45, 56 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
58 | | simpl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝜑) |
59 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → ¬ (𝐵‘𝑍) ≤ 𝐶) |
60 | 58, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) |
61 | 58, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) |
62 | 60, 61 | ltnled 10979 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐶 < (𝐵‘𝑍) ↔ ¬ (𝐵‘𝑍) ≤ 𝐶)) |
63 | 59, 62 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 < (𝐵‘𝑍)) |
64 | 7 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ∈ ℝ) |
65 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → (𝐵‘𝑍) ∈ ℝ) |
66 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 < (𝐵‘𝑍)) |
67 | 64, 65, 66 | ltled 10980 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ (𝐵‘𝑍)) |
68 | 67 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ (𝐵‘𝑍)) |
69 | | iftrue 4445 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) |
70 | 69 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝐵‘𝑍) ≤ 𝐷 → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
71 | 70 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
72 | 68, 71 | breqtrd 5079 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
73 | 52 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ 𝐷) |
74 | | iffalse 4448 |
. . . . . . . . . . . 12
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = 𝐷) |
75 | 74 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
76 | 75 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
77 | 73, 76 | breqtrd 5079 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
78 | 72, 77 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
79 | 58, 63, 78 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
80 | | iffalse 4448 |
. . . . . . . . 9
⊢ (¬
(𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) |
81 | 80 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) |
82 | 81 | breq1d 5063 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
83 | 79, 82 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
84 | 57, 83 | pm2.61dan 813 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
85 | | icossico 13005 |
. . . . 5
⊢ ((((𝐴‘𝑍) ∈ ℝ* ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) ∧ ((𝐴‘𝑍) ≤ (𝐴‘𝑍) ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
86 | 42, 39, 43, 84, 85 | syl22anc 839 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
87 | | volss 24430 |
. . . 4
⊢ ((((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol ∧ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol ∧ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ≤ (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
88 | 38, 41, 86, 87 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ≤ (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
89 | 10, 14, 26, 35, 88 | lemul1ad 11771 |
. 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
90 | | hsphoidmvle2.l |
. . . . 5
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
91 | 3 | ne0d 4250 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) |
92 | | hsphoidmvle2.h |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
93 | 92, 7, 15, 5 | hsphoif 43789 |
. . . . 5
⊢ (𝜑 → ((𝐻‘𝐶)‘𝐵):𝑋⟶ℝ) |
94 | 90, 15, 91, 1, 93 | hoidmvn0val 43797 |
. . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) |
95 | 93 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) |
96 | | volicore 43794 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) |
97 | 21, 95, 96 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) |
98 | 97 | recnd 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℂ) |
99 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
100 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (((𝐻‘𝐶)‘𝐵)‘𝑍)) |
101 | 99, 100 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) |
102 | 101 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) |
103 | 102 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) |
104 | 92, 7, 15, 5, 3 | hsphoival 43792 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) |
105 | 2 | eldifbd 3879 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
106 | 105 | iffalsed 4450 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) |
107 | 104, 106 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) |
108 | 107 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) |
109 | 108 | fveq2d 6721 |
. . . . . . 7
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
110 | 109 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
111 | 103, 110 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
112 | 15, 98, 3, 111 | fprodsplit1 42809 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))))) |
113 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐶 ∈ ℝ) |
114 | 15 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑋 ∈ Fin) |
115 | 5 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐵:𝑋⟶ℝ) |
116 | 92, 113, 114, 115, 20 | hsphoival 43792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶))) |
117 | | hsphoidmvle2.y |
. . . . . . . . . . . . 13
⊢ 𝑋 = (𝑌 ∪ {𝑍}) |
118 | 19, 117 | eleqtrdi 2848 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ (𝑌 ∪ {𝑍})) |
119 | | eldifn 4042 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → ¬ 𝑘 ∈ {𝑍}) |
120 | | elunnel2 42255 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (𝑌 ∪ {𝑍}) ∧ ¬ 𝑘 ∈ {𝑍}) → 𝑘 ∈ 𝑌) |
121 | 118, 119,
120 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑌) |
122 | 121 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑌) |
123 | 122 | iftrued 4447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶)) = (𝐵‘𝑘)) |
124 | 116, 123 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (𝐵‘𝑘)) |
125 | 124 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
126 | 125 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
127 | 126 | prodeq2dv 15485 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
128 | 127 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
129 | 94, 112, 128 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
130 | 92, 11, 15, 5 | hsphoif 43789 |
. . . . 5
⊢ (𝜑 → ((𝐻‘𝐷)‘𝐵):𝑋⟶ℝ) |
131 | 90, 15, 91, 1, 130 | hoidmvn0val 43797 |
. . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) |
132 | 130 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) |
133 | | volicore 43794 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) |
134 | 21, 132, 133 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) |
135 | 134 | recnd 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℂ) |
136 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (((𝐻‘𝐷)‘𝐵)‘𝑍)) |
137 | 99, 136 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) |
138 | 137 | fveq2d 6721 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) |
139 | 138 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) |
140 | 15, 135, 3, 139 | fprodsplit1 42809 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))))) |
141 | 92, 11, 15, 5, 3 | hsphoival 43792 |
. . . . . . . 8
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
142 | 105 | iffalsed 4450 |
. . . . . . . 8
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
143 | 141, 142 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
144 | 143 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
145 | 144 | fveq2d 6721 |
. . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
146 | 11 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐷 ∈ ℝ) |
147 | 92, 146, 114, 115, 20 | hsphoival 43792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷))) |
148 | 122 | iftrued 4447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷)) = (𝐵‘𝑘)) |
149 | 147, 148 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (𝐵‘𝑘)) |
150 | 149 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
151 | 150 | fveq2d 6721 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
152 | 151 | prodeq2dv 15485 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
153 | 145, 152 | oveq12d 7231 |
. . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
154 | 131, 140,
153 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
155 | 129, 154 | breq12d 5066 |
. 2
⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) ↔ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))))) |
156 | 89, 155 | mpbird 260 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵))) |