Step |
Hyp |
Ref |
Expression |
1 |
|
itg1val |
|- ( F e. dom S.1 -> ( S.1 ` F ) = sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) ) |
2 |
|
i1frn |
|- ( F e. dom S.1 -> ran F e. Fin ) |
3 |
|
difss |
|- ( ran F \ { 0 } ) C_ ran F |
4 |
|
ssfi |
|- ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin ) |
5 |
2 3 4
|
sylancl |
|- ( F e. dom S.1 -> ( ran F \ { 0 } ) e. Fin ) |
6 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
7 |
6
|
frnd |
|- ( F e. dom S.1 -> ran F C_ RR ) |
8 |
7
|
ssdifssd |
|- ( F e. dom S.1 -> ( ran F \ { 0 } ) C_ RR ) |
9 |
8
|
sselda |
|- ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> x e. RR ) |
10 |
|
i1fima2sn |
|- ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR ) |
11 |
9 10
|
remulcld |
|- ( ( F e. dom S.1 /\ x e. ( ran F \ { 0 } ) ) -> ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR ) |
12 |
5 11
|
fsumrecl |
|- ( F e. dom S.1 -> sum_ x e. ( ran F \ { 0 } ) ( x x. ( vol ` ( `' F " { x } ) ) ) e. RR ) |
13 |
1 12
|
eqeltrd |
|- ( F e. dom S.1 -> ( S.1 ` F ) e. RR ) |