Proof of Theorem hsphoidmvle2
Step | Hyp | Ref
| Expression |
1 | | hsphoidmvle2.a |
. . . . 5
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
2 | | hsphoidmvle2.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
3 | 2 | eldifad 3586 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
4 | 1, 3 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
5 | | hsphoidmvle2.b |
. . . . . 6
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
6 | 5, 3 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
7 | | hsphoidmvle2.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
8 | 6, 7 | ifcld 4131 |
. . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) |
9 | | volicore 40795 |
. . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) |
10 | 4, 8, 9 | syl2anc 693 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) |
11 | | hsphoidmvle2.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℝ) |
12 | 6, 11 | ifcld 4131 |
. . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) |
13 | | volicore 40795 |
. . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) |
14 | 4, 12, 13 | syl2anc 693 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) |
15 | | hsphoidmvle2.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
16 | | difssd 3738 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ⊆ 𝑋) |
17 | | ssfi 8180 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → (𝑋 ∖ {𝑍}) ∈ Fin) |
18 | 15, 16, 17 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ∈ Fin) |
19 | | eldifi 3732 |
. . . . . 6
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑋) |
20 | 19 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑋) |
21 | 1 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
22 | 5 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
23 | | volicore 40795 |
. . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
24 | 21, 22, 23 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
25 | 20, 24 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
26 | 18, 25 | fprodrecl 14683 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
27 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑘𝜑 |
28 | 20, 21 | syldan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐴‘𝑘) ∈ ℝ) |
29 | 20, 22 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈ ℝ) |
30 | 29 | rexrd 10089 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈
ℝ*) |
31 | | icombl 23332 |
. . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
32 | 28, 30, 31 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
33 | | volge0 40177 |
. . . . 5
⊢ (((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol → 0 ≤
(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 0 ≤ (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
35 | 27, 18, 25, 34 | fprodge0 14724 |
. . 3
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
36 | 8 | rexrd 10089 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈
ℝ*) |
37 | | icombl 23332 |
. . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) |
38 | 4, 36, 37 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) |
39 | 12 | rexrd 10089 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈
ℝ*) |
40 | | icombl 23332 |
. . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) |
41 | 4, 39, 40 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) |
42 | 4 | rexrd 10089 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) |
43 | 4 | leidd 10594 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ≤ (𝐴‘𝑍)) |
44 | 6 | leidd 10594 |
. . . . . . . 8
⊢ (𝜑 → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) |
45 | 44 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) |
46 | | iftrue 4092 |
. . . . . . . . 9
⊢ ((𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) |
47 | 46 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) |
48 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) |
49 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) |
50 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐷 ∈ ℝ) |
51 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐶) |
52 | | hsphoidmvle2.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ≤ 𝐷) |
53 | 52 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ 𝐷) |
54 | 48, 49, 50, 51, 53 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐷) |
55 | 54 | iftrued 4094 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) |
56 | 47, 55 | breq12d 4666 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ (𝐵‘𝑍) ≤ (𝐵‘𝑍))) |
57 | 45, 56 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
58 | | simpl 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝜑) |
59 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → ¬ (𝐵‘𝑍) ≤ 𝐶) |
60 | 58, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) |
61 | 58, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) |
62 | 60, 61 | ltnled 10184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐶 < (𝐵‘𝑍) ↔ ¬ (𝐵‘𝑍) ≤ 𝐶)) |
63 | 59, 62 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 < (𝐵‘𝑍)) |
64 | 7 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ∈ ℝ) |
65 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → (𝐵‘𝑍) ∈ ℝ) |
66 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 < (𝐵‘𝑍)) |
67 | 64, 65, 66 | ltled 10185 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ (𝐵‘𝑍)) |
68 | 67 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ (𝐵‘𝑍)) |
69 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) |
70 | 69 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝐵‘𝑍) ≤ 𝐷 → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
71 | 70 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
72 | 68, 71 | breqtrd 4679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
73 | 52 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ 𝐷) |
74 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = 𝐷) |
75 | 74 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
76 | 75 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
77 | 73, 76 | breqtrd 4679 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
78 | 72, 77 | pm2.61dan 832 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
79 | 58, 63, 78 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
80 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
(𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) |
81 | 80 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) |
82 | 81 | breq1d 4663 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
83 | 79, 82 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
84 | 57, 83 | pm2.61dan 832 |
. . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
85 | | icossico 12243 |
. . . . 5
⊢ ((((𝐴‘𝑍) ∈ ℝ* ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) ∧ ((𝐴‘𝑍) ≤ (𝐴‘𝑍) ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
86 | 42, 39, 43, 84, 85 | syl22anc 1327 |
. . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
87 | | volss 23301 |
. . . 4
⊢ ((((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol ∧ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol ∧ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ≤ (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
88 | 38, 41, 86, 87 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ≤ (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
89 | 10, 14, 26, 35, 88 | lemul1ad 10963 |
. 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
90 | | hsphoidmvle2.l |
. . . . 5
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
91 | | ne0i 3921 |
. . . . . 6
⊢ (𝑍 ∈ 𝑋 → 𝑋 ≠ ∅) |
92 | 3, 91 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) |
93 | | hsphoidmvle2.h |
. . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
94 | 93, 7, 15, 5 | hsphoif 40790 |
. . . . 5
⊢ (𝜑 → ((𝐻‘𝐶)‘𝐵):𝑋⟶ℝ) |
95 | 90, 15, 92, 1, 94 | hoidmvn0val 40798 |
. . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) |
96 | 94 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) |
97 | | volicore 40795 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) |
98 | 21, 96, 97 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) |
99 | 98 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℂ) |
100 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) |
101 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (((𝐻‘𝐶)‘𝐵)‘𝑍)) |
102 | 100, 101 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) |
103 | 102 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) |
104 | 103 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) |
105 | 93, 7, 15, 5, 3 | hsphoival 40793 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) |
106 | 2 | eldifbd 3587 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
107 | 106 | iffalsed 4097 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) |
108 | 105, 107 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) |
109 | 108 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) |
110 | 109 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
111 | 110 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
112 | 104, 111 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) |
113 | 15, 99, 3, 112 | fprodsplit1 39825 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))))) |
114 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐶 ∈ ℝ) |
115 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑋 ∈ Fin) |
116 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐵:𝑋⟶ℝ) |
117 | 93, 114, 115, 116, 20 | hsphoival 40793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶))) |
118 | | hsphoidmvle2.y |
. . . . . . . . . . . . 13
⊢ 𝑋 = (𝑌 ∪ {𝑍}) |
119 | 19, 118 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ (𝑌 ∪ {𝑍})) |
120 | | eldifn 3733 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → ¬ 𝑘 ∈ {𝑍}) |
121 | | elunnel2 39198 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (𝑌 ∪ {𝑍}) ∧ ¬ 𝑘 ∈ {𝑍}) → 𝑘 ∈ 𝑌) |
122 | 119, 120,
121 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑌) |
123 | 122 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑌) |
124 | 123 | iftrued 4094 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶)) = (𝐵‘𝑘)) |
125 | 117, 124 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (𝐵‘𝑘)) |
126 | 125 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
127 | 126 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
128 | 127 | prodeq2dv 14653 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
129 | 128 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
130 | 95, 113, 129 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
131 | 93, 11, 15, 5 | hsphoif 40790 |
. . . . 5
⊢ (𝜑 → ((𝐻‘𝐷)‘𝐵):𝑋⟶ℝ) |
132 | 90, 15, 92, 1, 131 | hoidmvn0val 40798 |
. . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) |
133 | 131 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) |
134 | | volicore 40795 |
. . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) |
135 | 21, 133, 134 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) |
136 | 135 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℂ) |
137 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (((𝐻‘𝐷)‘𝐵)‘𝑍)) |
138 | 100, 137 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) |
139 | 138 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) |
140 | 139 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) |
141 | 15, 136, 3, 140 | fprodsplit1 39825 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))))) |
142 | 93, 11, 15, 5, 3 | hsphoival 40793 |
. . . . . . . 8
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
143 | 106 | iffalsed 4097 |
. . . . . . . 8
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
144 | 142, 143 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) |
145 | 144 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) |
146 | 145 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) |
147 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐷 ∈ ℝ) |
148 | 93, 147, 115, 116, 20 | hsphoival 40793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷))) |
149 | 123 | iftrued 4094 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷)) = (𝐵‘𝑘)) |
150 | 148, 149 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (𝐵‘𝑘)) |
151 | 150 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
152 | 151 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
153 | 152 | prodeq2dv 14653 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
154 | 146, 153 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
155 | 132, 141,
154 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
156 | 130, 155 | breq12d 4666 |
. 2
⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) ↔ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))))) |
157 | 89, 156 | mpbird 247 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵))) |