Proof of Theorem hsphoidmvle2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hsphoidmvle2.a | . . . . 5
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) | 
| 2 |  | hsphoidmvle2.z | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) | 
| 3 | 2 | eldifad 3963 | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑋) | 
| 4 | 1, 3 | ffvelcdmd 7105 | . . . 4
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) | 
| 5 |  | hsphoidmvle2.b | . . . . . 6
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) | 
| 6 | 5, 3 | ffvelcdmd 7105 | . . . . 5
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) | 
| 7 |  | hsphoidmvle2.c | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 8 | 6, 7 | ifcld 4572 | . . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) | 
| 9 |  | volicore 46596 | . . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) | 
| 10 | 4, 8, 9 | syl2anc 584 | . . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) ∈ ℝ) | 
| 11 |  | hsphoidmvle2.d | . . . . 5
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 12 | 6, 11 | ifcld 4572 | . . . 4
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) | 
| 13 |  | volicore 46596 | . . . 4
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ) → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) | 
| 14 | 4, 12, 13 | syl2anc 584 | . . 3
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) ∈ ℝ) | 
| 15 |  | hsphoidmvle2.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 16 |  | difssd 4137 | . . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ⊆ 𝑋) | 
| 17 |  | ssfi 9213 | . . . . 5
⊢ ((𝑋 ∈ Fin ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → (𝑋 ∖ {𝑍}) ∈ Fin) | 
| 18 | 15, 16, 17 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑋 ∖ {𝑍}) ∈ Fin) | 
| 19 |  | eldifi 4131 | . . . . . 6
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑋) | 
| 20 | 19 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑋) | 
| 21 | 1 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) | 
| 22 | 5 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) | 
| 23 |  | volicore 46596 | . . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 24 | 21, 22, 23 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 25 | 20, 24 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 26 | 18, 25 | fprodrecl 15989 | . . 3
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) | 
| 27 |  | nfv 1914 | . . . 4
⊢
Ⅎ𝑘𝜑 | 
| 28 | 20, 21 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐴‘𝑘) ∈ ℝ) | 
| 29 | 20, 22 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈ ℝ) | 
| 30 | 29 | rexrd 11311 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (𝐵‘𝑘) ∈
ℝ*) | 
| 31 |  | icombl 25599 | . . . . . 6
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) | 
| 32 | 28, 30, 31 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) | 
| 33 |  | volge0 45976 | . . . . 5
⊢ (((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol → 0 ≤
(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 34 | 32, 33 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 0 ≤ (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 35 | 27, 18, 25, 34 | fprodge0 16029 | . . 3
⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 36 | 8 | rexrd 11311 | . . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈
ℝ*) | 
| 37 |  | icombl 25599 | . . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) | 
| 38 | 4, 36, 37 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ∈ dom vol) | 
| 39 | 12 | rexrd 11311 | . . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈
ℝ*) | 
| 40 |  | icombl 25599 | . . . . 5
⊢ (((𝐴‘𝑍) ∈ ℝ ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) | 
| 41 | 4, 39, 40 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) ∈ dom vol) | 
| 42 | 4 | rexrd 11311 | . . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) | 
| 43 | 4 | leidd 11829 | . . . . 5
⊢ (𝜑 → (𝐴‘𝑍) ≤ (𝐴‘𝑍)) | 
| 44 | 6 | leidd 11829 | . . . . . . . 8
⊢ (𝜑 → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) | 
| 45 | 44 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ (𝐵‘𝑍)) | 
| 46 |  | iftrue 4531 | . . . . . . . . 9
⊢ ((𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) | 
| 47 | 46 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = (𝐵‘𝑍)) | 
| 48 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) | 
| 49 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) | 
| 50 | 11 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐷 ∈ ℝ) | 
| 51 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐶) | 
| 52 |  | hsphoidmvle2.e | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ≤ 𝐷) | 
| 53 | 52 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ 𝐷) | 
| 54 | 48, 49, 50, 51, 53 | letrd 11418 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ≤ 𝐷) | 
| 55 | 54 | iftrued 4533 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) | 
| 56 | 47, 55 | breq12d 5156 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ (𝐵‘𝑍) ≤ (𝐵‘𝑍))) | 
| 57 | 45, 56 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 58 |  | simpl 482 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝜑) | 
| 59 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → ¬ (𝐵‘𝑍) ≤ 𝐶) | 
| 60 | 58, 7 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ∈ ℝ) | 
| 61 | 58, 6 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐵‘𝑍) ∈ ℝ) | 
| 62 | 60, 61 | ltnled 11408 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (𝐶 < (𝐵‘𝑍) ↔ ¬ (𝐵‘𝑍) ≤ 𝐶)) | 
| 63 | 59, 62 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 < (𝐵‘𝑍)) | 
| 64 | 7 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ∈ ℝ) | 
| 65 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → (𝐵‘𝑍) ∈ ℝ) | 
| 66 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 < (𝐵‘𝑍)) | 
| 67 | 64, 65, 66 | ltled 11409 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ (𝐵‘𝑍)) | 
| 68 | 67 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ (𝐵‘𝑍)) | 
| 69 |  | iftrue 4531 | . . . . . . . . . . . 12
⊢ ((𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = (𝐵‘𝑍)) | 
| 70 | 69 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝐵‘𝑍) ≤ 𝐷 → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 71 | 70 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → (𝐵‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 72 | 68, 71 | breqtrd 5169 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 73 | 52 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ 𝐷) | 
| 74 |  | iffalse 4534 | . . . . . . . . . . . 12
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) = 𝐷) | 
| 75 | 74 | eqcomd 2743 | . . . . . . . . . . 11
⊢ (¬
(𝐵‘𝑍) ≤ 𝐷 → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 76 | 75 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐷 = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 77 | 73, 76 | breqtrd 5169 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) ∧ ¬ (𝐵‘𝑍) ≤ 𝐷) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 78 | 72, 77 | pm2.61dan 813 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < (𝐵‘𝑍)) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 79 | 58, 63, 78 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 80 |  | iffalse 4534 | . . . . . . . . 9
⊢ (¬
(𝐵‘𝑍) ≤ 𝐶 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) | 
| 81 | 80 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) = 𝐶) | 
| 82 | 81 | breq1d 5153 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → (if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ↔ 𝐶 ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) | 
| 83 | 79, 82 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐵‘𝑍) ≤ 𝐶) → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 84 | 57, 83 | pm2.61dan 813 | . . . . 5
⊢ (𝜑 → if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 85 |  | icossico 13457 | . . . . 5
⊢ ((((𝐴‘𝑍) ∈ ℝ* ∧ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷) ∈ ℝ*) ∧ ((𝐴‘𝑍) ≤ (𝐴‘𝑍) ∧ if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶) ≤ if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) | 
| 86 | 42, 39, 43, 84, 85 | syl22anc 839 | . . . 4
⊢ (𝜑 → ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) ⊆ ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) | 
| 87 |  | volss 25568 | . . . 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 12207 | . 2
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 90 |  | hsphoidmvle2.l | . . . . 5
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) | 
| 91 | 3 | ne0d 4342 | . . . . 5
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 92 |  | hsphoidmvle2.h | . . . . . 6
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) | 
| 93 | 92, 7, 15, 5 | hsphoif 46591 | . . . . 5
⊢ (𝜑 → ((𝐻‘𝐶)‘𝐵):𝑋⟶ℝ) | 
| 94 | 90, 15, 91, 1, 93 | hoidmvn0val 46599 | . . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) | 
| 95 | 93 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) | 
| 96 |  | volicore 46596 | . . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐶)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) | 
| 97 | 21, 95, 96 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℝ) | 
| 98 | 97 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) ∈ ℂ) | 
| 99 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑘 = 𝑍 → (𝐴‘𝑘) = (𝐴‘𝑍)) | 
| 100 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (((𝐻‘𝐶)‘𝐵)‘𝑍)) | 
| 101 | 99, 100 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) | 
| 102 | 101 | fveq2d 6910 | . . . . . . 7
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) | 
| 103 | 102 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)))) | 
| 104 | 92, 7, 15, 5, 3 | hsphoival 46594 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) | 
| 105 | 2 | eldifbd 3964 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) | 
| 106 | 105 | iffalsed 4536 | . . . . . . . . . 10
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) | 
| 107 | 104, 106 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (((𝐻‘𝐶)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)) | 
| 108 | 107 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) | 
| 109 | 108 | fveq2d 6910 | . . . . . . 7
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) | 
| 110 | 109 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐶)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) | 
| 111 | 103, 110 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶)))) | 
| 112 | 15, 98, 3, 111 | fprodsplit1 45608 | . . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))))) | 
| 113 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐶 ∈ ℝ) | 
| 114 | 15 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑋 ∈ Fin) | 
| 115 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐵:𝑋⟶ℝ) | 
| 116 | 92, 113, 114, 115, 20 | hsphoival 46594 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶))) | 
| 117 |  | hsphoidmvle2.y | . . . . . . . . . . . . 13
⊢ 𝑋 = (𝑌 ∪ {𝑍}) | 
| 118 | 19, 117 | eleqtrdi 2851 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ (𝑌 ∪ {𝑍})) | 
| 119 |  | eldifn 4132 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → ¬ 𝑘 ∈ {𝑍}) | 
| 120 |  | elunnel2 4155 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ (𝑌 ∪ {𝑍}) ∧ ¬ 𝑘 ∈ {𝑍}) → 𝑘 ∈ 𝑌) | 
| 121 | 118, 119,
120 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑋 ∖ {𝑍}) → 𝑘 ∈ 𝑌) | 
| 122 | 121 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝑘 ∈ 𝑌) | 
| 123 | 122 | iftrued 4533 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐶, (𝐵‘𝑘), 𝐶)) = (𝐵‘𝑘)) | 
| 124 | 116, 123 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐶)‘𝐵)‘𝑘) = (𝐵‘𝑘)) | 
| 125 | 124 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 126 | 125 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 127 | 126 | prodeq2dv 15958 | . . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 128 | 127 | oveq2d 7447 | . . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐶)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 129 | 94, 112, 128 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 130 | 92, 11, 15, 5 | hsphoif 46591 | . . . . 5
⊢ (𝜑 → ((𝐻‘𝐷)‘𝐵):𝑋⟶ℝ) | 
| 131 | 90, 15, 91, 1, 130 | hoidmvn0val 46599 | . . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) | 
| 132 | 130 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) | 
| 133 |  | volicore 46596 | . . . . . . 7
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝐻‘𝐷)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) | 
| 134 | 21, 132, 133 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℝ) | 
| 135 | 134 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) ∈ ℂ) | 
| 136 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑘 = 𝑍 → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (((𝐻‘𝐷)‘𝐵)‘𝑍)) | 
| 137 | 99, 136 | oveq12d 7449 | . . . . . . 7
⊢ (𝑘 = 𝑍 → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) | 
| 138 | 137 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 𝑍 → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) | 
| 139 | 138 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 = 𝑍) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)))) | 
| 140 | 15, 135, 3, 139 | fprodsplit1 45608 | . . . 4
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))))) | 
| 141 | 92, 11, 15, 5, 3 | hsphoival 46594 | . . . . . . . 8
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) | 
| 142 | 105 | iffalsed 4536 | . . . . . . . 8
⊢ (𝜑 → if(𝑍 ∈ 𝑌, (𝐵‘𝑍), if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 143 | 141, 142 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → (((𝐻‘𝐷)‘𝐵)‘𝑍) = if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)) | 
| 144 | 143 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → ((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍)) = ((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) | 
| 145 | 144 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) = (vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷)))) | 
| 146 | 11 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → 𝐷 ∈ ℝ) | 
| 147 | 92, 146, 114, 115, 20 | hsphoival 46594 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷))) | 
| 148 | 122 | iftrued 4533 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → if(𝑘 ∈ 𝑌, (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝐷, (𝐵‘𝑘), 𝐷)) = (𝐵‘𝑘)) | 
| 149 | 147, 148 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (((𝐻‘𝐷)‘𝐵)‘𝑘) = (𝐵‘𝑘)) | 
| 150 | 149 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → ((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 151 | 150 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝑍})) → (vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 152 | 151 | prodeq2dv 15958 | . . . . 5
⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | 
| 153 | 145, 152 | oveq12d 7449 | . . . 4
⊢ (𝜑 → ((vol‘((𝐴‘𝑍)[,)(((𝐻‘𝐷)‘𝐵)‘𝑍))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(((𝐻‘𝐷)‘𝐵)‘𝑘)))) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 154 | 131, 140,
153 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) = ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | 
| 155 | 129, 154 | breq12d 5156 | . 2
⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵)) ↔ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐶, (𝐵‘𝑍), 𝐶))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) ≤ ((vol‘((𝐴‘𝑍)[,)if((𝐵‘𝑍) ≤ 𝐷, (𝐵‘𝑍), 𝐷))) · ∏𝑘 ∈ (𝑋 ∖ {𝑍})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))))) | 
| 156 | 89, 155 | mpbird 257 | 1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵))) |