Metamath Proof Explorer

Theorem hoidmvval0

Description: The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvval0.p ⊢ Ⅎ 𝑗 𝜑
hoidmvval0.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hoidmvval0.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoidmvval0.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hoidmvval0.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
hoidmvval0.j ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
Assertion hoidmvval0 ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 hoidmvval0.p ⊢ Ⅎ 𝑗 𝜑
2 hoidmvval0.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
3 hoidmvval0.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
4 hoidmvval0.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5 hoidmvval0.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
6 hoidmvval0.j ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
7 id ⊢ ( 𝜑 → 𝜑 )
8 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑗 ) )
9 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑗 ) )
10 8 9 breq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ↔ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) )
11 10 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) ↔ ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
12 rexn0 ⊢ ( ∃ 𝑘 ∈ 𝑋 ( 𝐵 ‘ 𝑘 ) ≤ ( 𝐴 ‘ 𝑘 ) → 𝑋 ≠ ∅ )
13 11 12 sylbir ⊢ ( ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) → 𝑋 ≠ ∅ )
14 6 13 syl ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ Fin )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
18 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
19 2 15 16 17 18 hoidmvn0val ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
21 nfv ⊢ Ⅎ 𝑗 𝑋 ≠ ∅
22 1 21 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑋 ≠ ∅ )
23 nfv ⊢ Ⅎ 𝑗 ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0
24 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
25 nfcv ⊢ Ⅎ 𝑘 ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) )
26 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → 𝑋 ∈ Fin )
27 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
28 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
29 volicore ⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
30 27 28 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
32 31 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ∧ 𝑘 ∈ 𝑋 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℂ )
33 9 8 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) )
34 33 fveq2d ⊢ ( 𝑘 = 𝑗 → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) )
35 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → 𝑗 ∈ 𝑋 )
36 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑗 ) ∈ ℝ )
37 36 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℝ )
38 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
39 38 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ℝ )
40 volico ⊢ ( ( ( 𝐴 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑗 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) )
41 37 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) )
42 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
43 39 37 lenltd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ↔ ¬ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) ) )
44 42 43 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ¬ ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) )
45 44 iffalsed ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → if ( ( 𝐴 ‘ 𝑗 ) < ( 𝐵 ‘ 𝑗 ) , ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) , 0 ) = 0 )
46 41 45 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ( vol ‘ ( ( 𝐴 ‘ 𝑗 ) [,) ( 𝐵 ‘ 𝑗 ) ) ) = 0 )
47 24 25 26 32 34 35 46 fprod0 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
48 47 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) ∧ 𝑗 ∈ 𝑋 ∧ ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
49 48 3exp ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑗 ∈ 𝑋 → ( ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 ) ) )
50 22 23 49 rexlimd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑗 ∈ 𝑋 ( 𝐵 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 ) )
51 20 50 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 0 )
52 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 0 = 0 )
53 19 51 52 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )
54 7 14 53 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) = 0 )