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