Metamath Proof Explorer

Theorem hoidmvval0b

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

Proof

Step Hyp Ref Expression
1 hoidmvval0b.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
2 hoidmvval0b.x ⊢ φ → X ∈ Fin
3 hoidmvval0b.a ⊢ φ → A : X ⟶ ℝ
4 fveq2 ⊢ X = ∅ → L ⁡ X = L ⁡ ∅
5 4 oveqd ⊢ X = ∅ → A L ⁡ X A = A L ⁡ ∅ A
6 5 adantl ⊢ φ ∧ X = ∅ → A L ⁡ X A = A L ⁡ ∅ A
7 3 adantr ⊢ φ ∧ X = ∅ → A : X ⟶ ℝ
8 feq2 ⊢ X = ∅ → A : X ⟶ ℝ ↔ A : ∅ ⟶ ℝ
9 8 adantl ⊢ φ ∧ X = ∅ → A : X ⟶ ℝ ↔ A : ∅ ⟶ ℝ
10 7 9 mpbid ⊢ φ ∧ X = ∅ → A : ∅ ⟶ ℝ
11 1 10 10 hoidmv0val ⊢ φ ∧ X = ∅ → A L ⁡ ∅ A = 0
12 6 11 eqtrd ⊢ φ ∧ X = ∅ → A L ⁡ X A = 0
13 nfv ⊢ Ⅎ j φ ∧ ¬ X = ∅
14 2 adantr ⊢ φ ∧ ¬ X = ∅ → X ∈ Fin
15 3 adantr ⊢ φ ∧ ¬ X = ∅ → A : X ⟶ ℝ
16 neqne ⊢ ¬ X = ∅ → X ≠ ∅
17 n0 ⊢ X ≠ ∅ ↔ ∃ j j ∈ X
18 16 17 sylib ⊢ ¬ X = ∅ → ∃ j j ∈ X
19 18 adantl ⊢ φ ∧ ¬ X = ∅ → ∃ j j ∈ X
20 simpr ⊢ φ ∧ j ∈ X → j ∈ X
21 3 ffvelrnda ⊢ φ ∧ j ∈ X → A ⁡ j ∈ ℝ
22 eqidd ⊢ φ ∧ j ∈ X → A ⁡ j = A ⁡ j
23 21 22 eqled ⊢ φ ∧ j ∈ X → A ⁡ j ≤ A ⁡ j
24 20 23 jca ⊢ φ ∧ j ∈ X → j ∈ X ∧ A ⁡ j ≤ A ⁡ j
25 24 ex ⊢ φ → j ∈ X → j ∈ X ∧ A ⁡ j ≤ A ⁡ j
26 25 adantr ⊢ φ ∧ ¬ X = ∅ → j ∈ X → j ∈ X ∧ A ⁡ j ≤ A ⁡ j
27 26 eximdv ⊢ φ ∧ ¬ X = ∅ → ∃ j j ∈ X → ∃ j j ∈ X ∧ A ⁡ j ≤ A ⁡ j
28 19 27 mpd ⊢ φ ∧ ¬ X = ∅ → ∃ j j ∈ X ∧ A ⁡ j ≤ A ⁡ j
29 df-rex ⊢ ∃ j ∈ X A ⁡ j ≤ A ⁡ j ↔ ∃ j j ∈ X ∧ A ⁡ j ≤ A ⁡ j
30 28 29 sylibr ⊢ φ ∧ ¬ X = ∅ → ∃ j ∈ X A ⁡ j ≤ A ⁡ j
31 13 1 14 15 15 30 hoidmvval0 ⊢ φ ∧ ¬ X = ∅ → A L ⁡ X A = 0
32 12 31 pm2.61dan ⊢ φ → A L ⁡ X A = 0