Step |
Hyp |
Ref |
Expression |
1 |
|
rneq |
⊢ ( 𝑓 = 𝐹 → ran 𝑓 = ran 𝐹 ) |
2 |
1
|
difeq1d |
⊢ ( 𝑓 = 𝐹 → ( ran 𝑓 ∖ { 0 } ) = ( ran 𝐹 ∖ { 0 } ) ) |
3 |
|
cnveq |
⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 ) |
4 |
3
|
imaeq1d |
⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ { 𝑥 } ) = ( ◡ 𝐹 “ { 𝑥 } ) ) |
5 |
4
|
fveq2d |
⊢ ( 𝑓 = 𝐹 → ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) = ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑓 = 𝐹 → ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ) → ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ) |
8 |
2 7
|
sumeq12dv |
⊢ ( 𝑓 = 𝐹 → Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ) |
9 |
|
df-itg1 |
⊢ ∫1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ) |
10 |
|
sumex |
⊢ Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ∈ V |
11 |
8 9 10
|
fvmpt |
⊢ ( 𝐹 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ) |
12 |
|
sumex |
⊢ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ∈ V |
13 |
12 9
|
dmmpti |
⊢ dom ∫1 = { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } |
14 |
11 13
|
eleq2s |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) ) |