Step |
Hyp |
Ref |
Expression |
1 |
|
ovolfs2.1 |
⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 ) |
2 |
|
ovolfcl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
3 |
|
ovolioo |
⊢ ( ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
5 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
6 |
|
rexpssxrxp |
⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) |
7 |
5 6
|
sstri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) |
8 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
9 |
7 8
|
sselid |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ* × ℝ* ) ) |
10 |
|
1st2nd2 |
⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ* × ℝ* ) → ( 𝐹 ‘ 𝑛 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
12 |
11
|
fveq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) ) |
13 |
|
df-ov |
⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) 〉 ) |
14 |
12 13
|
eqtr4di |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
15 |
14
|
fveq2d |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( vol* ‘ ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) ) |
16 |
1
|
ovolfsval |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) |
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
|
ffvelrnda |
⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ℝ* × ℝ* ) ) → ( (,) ‘ 𝑥 ) ∈ 𝒫 ℝ ) |
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* ∘ (,) ) ∘ 𝐹 ) ) |