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 ⊢ Ⅎ j φ
hoidmvval0.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
hoidmvval0.x ⊢ φ → X ∈ Fin
hoidmvval0.a ⊢ φ → A : X ⟶ ℝ
hoidmvval0.b ⊢ φ → B : X ⟶ ℝ
hoidmvval0.j ⊢ φ → ∃ j ∈ X B ⁡ j ≤ A ⁡ j
Assertion hoidmvval0 ⊢ φ → A L ⁡ X B = 0

Proof

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