ovolfs2

Description: Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Hypothesis	ovolfs2.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
	Assertion	ovolfs2	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( ( vol* ∘ (,) ) ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		ovolfs2.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
3		ovolioo	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
4	2 3	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
5		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
7	5 6	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
8		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
9	7 8	sselid	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ^* × ℝ^* ) )
10		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ^* × ℝ^* ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
11	9 10	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
12	11	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
13		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
14	12 13	eqtr4di	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
15	14	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
16	1	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
17	4 15 16	3eqtr4rd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
18	17	mpteq2dva	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( 𝑛 ∈ ℕ ↦ ( 𝐺 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
19	1	ovolfsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )
20	19	feqmptd	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 𝐺 ‘ 𝑛 ) ) )
21		id	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
22	21	feqmptd	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ 𝑛 ) ) )
23		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
24	23	a1i	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ )
25	24	ffvelcdmda	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ℝ^* × ℝ^* ) ) → ( (,) ‘ 𝑥 ) ∈ 𝒫 ℝ )
26	24	feqmptd	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → (,) = ( 𝑥 ∈ ( ℝ^* × ℝ^* ) ↦ ( (,) ‘ 𝑥 ) ) )
27		ovolf	⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
28	27	a1i	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) )
29	28	feqmptd	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → vol* = ( 𝑦 ∈ 𝒫 ℝ ↦ ( vol* ‘ 𝑦 ) ) )
30		fveq2	⊢ ( 𝑦 = ( (,) ‘ 𝑥 ) → ( vol* ‘ 𝑦 ) = ( vol* ‘ ( (,) ‘ 𝑥 ) ) )
31	25 26 29 30	fmptco	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( vol* ∘ (,) ) = ( 𝑥 ∈ ( ℝ^* × ℝ^* ) ↦ ( vol* ‘ ( (,) ‘ 𝑥 ) ) ) )
32		2fveq3	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( vol* ‘ ( (,) ‘ 𝑥 ) ) = ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
33	9 22 31 32	fmptco	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( vol* ∘ (,) ) ∘ 𝐹 ) = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
34	18 20 33	3eqtr4d	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 = ( ( vol* ∘ (,) ) ∘ 𝐹 ) )

Metamath Proof Explorer

Theorem ovolfs2

Proof