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 ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
hoidmvval0b.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoidmvval0b.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
Assertion hoidmvval0b ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 hoidmvval0b.l ⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
2 hoidmvval0b.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoidmvval0b.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4 fveq2 ⊢ ( 𝑋 = ∅ → ( 𝐿 ‘ 𝑋 ) = ( 𝐿 ‘ ∅ ) )
5 4 oveqd ⊢ ( 𝑋 = ∅ → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐴 ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐴 ) )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
8 feq2 ⊢ ( 𝑋 = ∅ → ( 𝐴 : 𝑋 ⟶ ℝ ↔ 𝐴 : ∅ ⟶ ℝ ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 : 𝑋 ⟶ ℝ ↔ 𝐴 : ∅ ⟶ ℝ ) )
10 7 9 mpbid ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 : ∅ ⟶ ℝ )
11 1 10 10 hoidmv0val ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ ∅ ) 𝐴 ) = 0 )
12 6 11 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = 0 )
13 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ¬ 𝑋 = ∅ )
14 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
15 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
16 neqne ⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
17 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑗 𝑗 ∈ 𝑋 )
18 16 17 sylib ⊢ ( ¬ 𝑋 = ∅ → ∃ 𝑗 𝑗 ∈ 𝑋 )
19 18 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑗 𝑗 ∈ 𝑋 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑗 ∈ 𝑋 )
21 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑗 ) ∈ ℝ )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
23 21 22 eqled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
24 20 23 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) )
25 24 ex ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑋 → ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 𝑗 ∈ 𝑋 → ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ) )
27 26 eximdv ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ∃ 𝑗 𝑗 ∈ 𝑋 → ∃ 𝑗 ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) ) )
28 19 27 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑗 ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) )
29 df-rex ⊢ ( ∃ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ↔ ∃ 𝑗 ( 𝑗 ∈ 𝑋 ∧ ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) ) )
30 28 29 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑗 ∈ 𝑋 ( 𝐴 ‘ 𝑗 ) ≤ ( 𝐴 ‘ 𝑗 ) )
31 13 1 14 15 15 30 hoidmvval0 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = 0 )
32 12 31 pm2.61dan ⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐴 ) = 0 )