Step |
Hyp |
Ref |
Expression |
0 |
|
citg1 |
⊢ ∫1 |
1 |
|
vf |
⊢ 𝑓 |
2 |
|
vg |
⊢ 𝑔 |
3 |
|
cmbf |
⊢ MblFn |
4 |
2
|
cv |
⊢ 𝑔 |
5 |
|
cr |
⊢ ℝ |
6 |
5 5 4
|
wf |
⊢ 𝑔 : ℝ ⟶ ℝ |
7 |
4
|
crn |
⊢ ran 𝑔 |
8 |
|
cfn |
⊢ Fin |
9 |
7 8
|
wcel |
⊢ ran 𝑔 ∈ Fin |
10 |
|
cvol |
⊢ vol |
11 |
4
|
ccnv |
⊢ ◡ 𝑔 |
12 |
|
cc0 |
⊢ 0 |
13 |
12
|
csn |
⊢ { 0 } |
14 |
5 13
|
cdif |
⊢ ( ℝ ∖ { 0 } ) |
15 |
11 14
|
cima |
⊢ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) |
16 |
15 10
|
cfv |
⊢ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) |
17 |
16 5
|
wcel |
⊢ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ |
18 |
6 9 17
|
w3a |
⊢ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) |
19 |
18 2 3
|
crab |
⊢ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } |
20 |
|
vx |
⊢ 𝑥 |
21 |
1
|
cv |
⊢ 𝑓 |
22 |
21
|
crn |
⊢ ran 𝑓 |
23 |
22 13
|
cdif |
⊢ ( ran 𝑓 ∖ { 0 } ) |
24 |
20
|
cv |
⊢ 𝑥 |
25 |
|
cmul |
⊢ · |
26 |
21
|
ccnv |
⊢ ◡ 𝑓 |
27 |
24
|
csn |
⊢ { 𝑥 } |
28 |
26 27
|
cima |
⊢ ( ◡ 𝑓 “ { 𝑥 } ) |
29 |
28 10
|
cfv |
⊢ ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) |
30 |
24 29 25
|
co |
⊢ ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) |
31 |
23 30 20
|
csu |
⊢ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) |
32 |
1 19 31
|
cmpt |
⊢ ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ) |
33 |
0 32
|
wceq |
⊢ ∫1 = ( 𝑓 ∈ { 𝑔 ∈ MblFn ∣ ( 𝑔 : ℝ ⟶ ℝ ∧ ran 𝑔 ∈ Fin ∧ ( vol ‘ ( ◡ 𝑔 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) } ↦ Σ 𝑥 ∈ ( ran 𝑓 ∖ { 0 } ) ( 𝑥 · ( vol ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ) |