ovnval2

Description: Value of the Lebesgue outer measure of a subset A of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ovnval2.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnval2.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
3		ovnval2.3	⊢ 𝑀 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
4	1	ovnval	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) = ( 𝑦 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) ) ) )
5		biidd	⊢ ( 𝑦 = 𝐴 → ( 𝑋 = ∅ ↔ 𝑋 = ∅ ) )
6		sseq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ↔ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
7	6	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
9	8	rabbidv	⊢ ( 𝑦 = 𝐴 → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
10	9 3	eqtr4di	⊢ ( 𝑦 = 𝐴 → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = 𝑀 )
11	10	infeq1d	⊢ ( 𝑦 = 𝐴 → inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) = inf ( 𝑀 , ℝ^* , < ) )
12	5 11	ifbieq2d	⊢ ( 𝑦 = 𝐴 → if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) ) = if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ^* , < ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) ) = if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ^* , < ) ) )
14		ovexd	⊢ ( 𝜑 → ( ℝ ↑_m 𝑋 ) ∈ V )
15	14 2	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
16		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) ) )
17	15 16	syl	⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) ↔ 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) ) )
18	2 17	mpbird	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ( ℝ ↑_m 𝑋 ) )
19		c0ex	⊢ 0 ∈ V
20	19	a1i	⊢ ( 𝜑 → 0 ∈ V )
21	3	infeq1i	⊢ inf ( 𝑀 , ℝ^* , < ) = inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < )
22		xrltso	⊢ < Or ℝ^*
23	22	infex	⊢ inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) ∈ V
24	23	a1i	⊢ ( 𝜑 → inf ( { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ^* , < ) ∈ V )
25	21 24	eqeltrid	⊢ ( 𝜑 → inf ( 𝑀 , ℝ^* , < ) ∈ V )
26	20 25	ifcld	⊢ ( 𝜑 → if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ^* , < ) ) ∈ V )
27	4 13 18 26	fvmptd	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = if ( 𝑋 = ∅ , 0 , inf ( 𝑀 , ℝ^* , < ) ) )

Metamath Proof Explorer

Theorem ovnval2

Proof