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 ffvelrnda ( ( 𝜑𝑗𝑋 ) → ( 𝐴𝑗 ) ∈ ℝ )
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 )