Proof of Theorem hoidifhspdmvle
Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . 3
⊢
Ⅎ𝑘𝜑 |
2 | | hoidifhspdmvle.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
3 | | hoidifhspdmvle.d |
. . . . . 6
⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) |
4 | | hoidifhspdmvle.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | hoidifhspdmvle.a |
. . . . . 6
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
6 | 3, 4, 2, 5 | hoidifhspf 44046 |
. . . . 5
⊢ (𝜑 → ((𝐷‘𝑌)‘𝐴):𝑋⟶ℝ) |
7 | 6 | ffvelrnda 6943 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐷‘𝑌)‘𝐴)‘𝑘) ∈ ℝ) |
8 | | hoidifhspdmvle.b |
. . . . 5
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
9 | 8 | ffvelrnda 6943 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
10 | | volicore 44009 |
. . . 4
⊢
(((((𝐷‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
11 | 7, 9, 10 | syl2anc 583 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
12 | 9 | rexrd 10956 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
13 | | icombl 24633 |
. . . . 5
⊢
(((((𝐷‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) →
((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
14 | 7, 12, 13 | syl2anc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
15 | | volge0 43392 |
. . . 4
⊢
(((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol → 0 ≤
(vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) |
16 | 14, 15 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 0 ≤ (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) |
17 | 5 | ffvelrnda 6943 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
18 | | volicore 44009 |
. . . 4
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
19 | 17, 9, 18 | syl2anc 583 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
20 | | icombl 24633 |
. . . . 5
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
21 | 17, 12, 20 | syl2anc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol) |
22 | 17 | rexrd 10956 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
23 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑌 ∈ ℝ) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ) |
25 | 17 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝐴‘𝑘) ∈ ℝ) |
26 | | max2 12850 |
. . . . . . . 8
⊢ ((𝑌 ∈ ℝ ∧ (𝐴‘𝑘) ∈ ℝ) → (𝐴‘𝑘) ≤ if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌)) |
27 | 24, 25, 26 | syl2anc 583 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝐴‘𝑘) ≤ if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌)) |
28 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin) |
29 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴:𝑋⟶ℝ) |
30 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
31 | 3, 23, 28, 29, 30 | hoidifhspval3 44047 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (((𝐷‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘))) |
32 | 31 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝐷‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘))) |
33 | | iftrue 4462 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌)) |
34 | 33 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌)) |
35 | 32, 34 | eqtr2d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌) = (((𝐷‘𝑌)‘𝐴)‘𝑘)) |
36 | 27, 35 | breqtrd 5096 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝐴‘𝑘) ≤ (((𝐷‘𝑌)‘𝐴)‘𝑘)) |
37 | 17 | leidd 11471 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐴‘𝑘)) |
38 | 37 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝐴‘𝑘) ≤ (𝐴‘𝑘)) |
39 | 31 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝐷‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘))) |
40 | | iffalse 4465 |
. . . . . . . . 9
⊢ (¬
𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘)) |
41 | 40 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘)) |
42 | 39, 41 | eqtr2d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝐴‘𝑘) = (((𝐷‘𝑌)‘𝐴)‘𝑘)) |
43 | 38, 42 | breqtrd 5096 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝐴‘𝑘) ≤ (((𝐷‘𝑌)‘𝐴)‘𝑘)) |
44 | 36, 43 | pm2.61dan 809 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (((𝐷‘𝑌)‘𝐴)‘𝑘)) |
45 | 9 | leidd 11471 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ≤ (𝐵‘𝑘)) |
46 | | icossico 13078 |
. . . . 5
⊢ ((((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) ∧ ((𝐴‘𝑘) ≤ (((𝐷‘𝑌)‘𝐴)‘𝑘) ∧ (𝐵‘𝑘) ≤ (𝐵‘𝑘))) → ((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
47 | 22, 12, 44, 45, 46 | syl22anc 835 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
48 | | volss 24602 |
. . . 4
⊢
((((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol ∧ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom vol ∧ ((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ≤ (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
49 | 14, 21, 47, 48 | syl3anc 1369 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ≤ (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
50 | 1, 2, 11, 16, 19, 49 | fprodle 15634 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
51 | | hoidifhspdmvle.l |
. . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
52 | | hoidifhspdmvle.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ 𝑋) |
53 | 52 | ne0d 4266 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
54 | 51, 2, 53, 6, 8 | hoidmvn0val 44012 |
. . 3
⊢ (𝜑 → (((𝐷‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) |
55 | 51, 2, 53, 5, 8 | hoidmvn0val 44012 |
. . 3
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
56 | 54, 55 | breq12d 5083 |
. 2
⊢ (𝜑 → ((((𝐷‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ≤ (𝐴(𝐿‘𝑋)𝐵) ↔ ∏𝑘 ∈ 𝑋 (vol‘((((𝐷‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) |
57 | 50, 56 | mpbird 256 |
1
⊢ (𝜑 → (((𝐷‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ≤ (𝐴(𝐿‘𝑋)𝐵)) |