Theorem ovnn0val

Description: The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnn0val.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnn0val.2	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	ovnn0val.3	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ovnn0val.4	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
Assertion	ovnn0val	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovnn0val.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnn0val.2	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		ovnn0val.3	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
4		ovnn0val.4	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
5	1 3 4	ovnval2	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) )
6	2	neneqd	⊢ ( 𝜑 → ¬ 𝑋 = ∅ )
7	6	iffalsed	⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ* , < ) ) = inf ( 𝑀 , ℝ* , < ) )
8	5 7	eqtrd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )