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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
11 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
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 ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) ( 𝐿 ‘ 𝑋 ) 𝐵 ) ≤ ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )