Step |
Hyp |
Ref |
Expression |
1 |
|
i1fpos.1 |
⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
2 |
|
simpr |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
3 |
2
|
biantrurd |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) ) |
4 |
|
i1ff |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ ) |
5 |
4
|
ffvelrnda |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
6 |
5
|
biantrurd |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) ) |
7 |
|
elrege0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
8 |
6 7
|
bitr4di |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) |
9 |
4
|
adantr |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ ) |
10 |
|
ffn |
⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ ) |
11 |
|
elpreima |
⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) ) |
12 |
9 10 11
|
3syl |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) ) ) |
13 |
3 8 12
|
3bitr4d |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ) ) |
14 |
13
|
ifbid |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
15 |
14
|
mpteq2dva |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
16 |
1 15
|
syl5eq |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
17 |
|
i1fima |
⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ∈ dom vol ) |
18 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
19 |
18
|
i1fres |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ) |
20 |
17 19
|
mpdan |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 0 [,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ) |
21 |
16 20
|
eqeltrd |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐺 ∈ dom ∫1 ) |