Definition df-ovoln

Description: Define the outer measure for the space of multidimensional real numbers. The cardinality of x is the dimension of the space modeled. Definition 115C of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	df-ovoln	⊢ voln* = ( 𝑥 ∈ Fin ↦ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		covoln	⊢ voln*
1		vx	⊢ 𝑥
2		cfn	⊢ Fin
3		vy	⊢ 𝑦
4		cr	⊢ ℝ
5		cmap	⊢ ↑m
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( ℝ ↑m 𝑥 )
8	7	cpw	⊢ 𝒫 ( ℝ ↑m 𝑥 )
9		c0	⊢ ∅
10	6 9	wceq	⊢ 𝑥 = ∅
11		cc0	⊢ 0
12		vz	⊢ 𝑧
13		cxr	⊢ ℝ*
14		vi	⊢ 𝑖
15	4 4	cxp	⊢ ( ℝ × ℝ )
16	15 6 5	co	⊢ ( ( ℝ × ℝ ) ↑m 𝑥 )
17		cn	⊢ ℕ
18	16 17 5	co	⊢ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ )
19	3	cv	⊢ 𝑦
20		vj	⊢ 𝑗
21		vk	⊢ 𝑘
22		cico	⊢ [,)
23	14	cv	⊢ 𝑖
24	20	cv	⊢ 𝑗
25	24 23	cfv	⊢ ( 𝑖 ‘ 𝑗 )
26	22 25	ccom	⊢ ( [,) ∘ ( 𝑖 ‘ 𝑗 ) )
27	21	cv	⊢ 𝑘
28	27 26	cfv	⊢ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 )
29	21 6 28	cixp	⊢ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 )
30	20 17 29	ciun	⊢ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 )
31	19 30	wss	⊢ 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 )
32	12	cv	⊢ 𝑧
33		csumge0	⊢ Σ^
34		cvol	⊢ vol
35	28 34	cfv	⊢ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
36	6 35 21	cprod	⊢ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
37	20 17 36	cmpt	⊢ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
38	37 33	cfv	⊢ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
39	32 38	wceq	⊢ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) )
40	31 39	wa	⊢ ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
41	40 14 18	wrex	⊢ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
42	41 12 13	crab	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
43		clt	⊢ <
44	42 13 43	cinf	⊢ inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < )
45	10 11 44	cif	⊢ if ( 𝑥 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) )
46	3 8 45	cmpt	⊢ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) )
47	1 2 46	cmpt	⊢ ( 𝑥 ∈ Fin ↦ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) )
48	0 47	wceq	⊢ voln* = ( 𝑥 ∈ Fin ↦ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑥 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑥 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) )