Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ovoln Structured version   Visualization version   GIF version

Definition df-ovoln 41257
Description: Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Assertion
Ref Expression
df-ovoln voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < ))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑖,𝑗,𝑘

Detailed syntax breakdown of Definition df-ovoln
StepHypRef Expression
1 covoln 41256 . 2 class voln*
2 vx . . 3 setvar 𝑥
3 cfn 8121 . . 3 class Fin
4 vy . . . 4 setvar 𝑦
5 cr 10127 . . . . . 6 class
62cv 1631 . . . . . 6 class 𝑥
7 cmap 8023 . . . . . 6 class 𝑚
85, 6, 7co 6813 . . . . 5 class (ℝ ↑𝑚 𝑥)
98cpw 4302 . . . 4 class 𝒫 (ℝ ↑𝑚 𝑥)
10 c0 4058 . . . . . 6 class
116, 10wceq 1632 . . . . 5 wff 𝑥 = ∅
12 cc0 10128 . . . . 5 class 0
134cv 1631 . . . . . . . . . 10 class 𝑦
14 vj . . . . . . . . . . 11 setvar 𝑗
15 cn 11212 . . . . . . . . . . 11 class
16 vk . . . . . . . . . . . 12 setvar 𝑘
1716cv 1631 . . . . . . . . . . . . 13 class 𝑘
18 cico 12370 . . . . . . . . . . . . . 14 class [,)
1914cv 1631 . . . . . . . . . . . . . . 15 class 𝑗
20 vi . . . . . . . . . . . . . . . 16 setvar 𝑖
2120cv 1631 . . . . . . . . . . . . . . 15 class 𝑖
2219, 21cfv 6049 . . . . . . . . . . . . . 14 class (𝑖𝑗)
2318, 22ccom 5270 . . . . . . . . . . . . 13 class ([,) ∘ (𝑖𝑗))
2417, 23cfv 6049 . . . . . . . . . . . 12 class (([,) ∘ (𝑖𝑗))‘𝑘)
2516, 6, 24cixp 8074 . . . . . . . . . . 11 class X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘)
2614, 15, 25ciun 4672 . . . . . . . . . 10 class 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘)
2713, 26wss 3715 . . . . . . . . 9 wff 𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘)
28 vz . . . . . . . . . . 11 setvar 𝑧
2928cv 1631 . . . . . . . . . 10 class 𝑧
30 cvol 23432 . . . . . . . . . . . . . 14 class vol
3124, 30cfv 6049 . . . . . . . . . . . . 13 class (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))
326, 31, 16cprod 14834 . . . . . . . . . . . 12 class 𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))
3314, 15, 32cmpt 4881 . . . . . . . . . . 11 class (𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))
34 csumge0 41082 . . . . . . . . . . 11 class Σ^
3533, 34cfv 6049 . . . . . . . . . 10 class ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))
3629, 35wceq 1632 . . . . . . . . 9 wff 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))
3727, 36wa 383 . . . . . . . 8 wff (𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))
385, 5cxp 5264 . . . . . . . . . 10 class (ℝ × ℝ)
3938, 6, 7co 6813 . . . . . . . . 9 class ((ℝ × ℝ) ↑𝑚 𝑥)
4039, 15, 7co 6813 . . . . . . . 8 class (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)
4137, 20, 40wrex 3051 . . . . . . 7 wff 𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))
42 cxr 10265 . . . . . . 7 class *
4341, 28, 42crab 3054 . . . . . 6 class {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}
44 clt 10266 . . . . . 6 class <
4543, 42, 44cinf 8512 . . . . 5 class inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < )
4611, 12, 45cif 4230 . . . 4 class if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < ))
474, 9, 46cmpt 4881 . . 3 class (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < )))
482, 3, 47cmpt 4881 . 2 class (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < ))))
491, 48wceq 1632 1 wff voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 𝑗 ∈ ℕ X𝑘𝑥 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑥 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))}, ℝ*, < ))))
Colors of variables: wff setvar class
This definition is referenced by:  ovnval  41261
  Copyright terms: Public domain W3C validator