Metamath Proof Explorer


Theorem hoidifhspdmvle

Description: The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoidifhspdmvle.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
hoidifhspdmvle.x ( 𝜑𝑋 ∈ Fin )
hoidifhspdmvle.a ( 𝜑𝐴 : 𝑋 ⟶ ℝ )
hoidifhspdmvle.b ( 𝜑𝐵 : 𝑋 ⟶ ℝ )
hoidifhspdmvle.k ( 𝜑𝐾𝑋 )
hoidifhspdmvle.d 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑋 ↦ if ( = 𝐾 , if ( 𝑥 ≤ ( 𝑐 ) , ( 𝑐 ) , 𝑥 ) , ( 𝑐 ) ) ) ) )
hoidifhspdmvle.y ( 𝜑𝑌 ∈ ℝ )
Assertion hoidifhspdmvle ( 𝜑 → ( ( ( 𝐷𝑌 ) ‘ 𝐴 ) ( 𝐿𝑋 ) 𝐵 ) ≤ ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) )

Proof

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 ( 𝜑 → ( ( ( 𝐷𝑌 ) ‘ 𝐴 ) ( 𝐿𝑋 ) 𝐵 ) ≤ ( 𝐴 ( 𝐿𝑋 ) 𝐵 ) )