Step |
Hyp |
Ref |
Expression |
1 |
|
itg1val |
โข ( ๐น โ dom โซ1 โ ( โซ1 โ ๐น ) = ฮฃ ๐ฅ โ ( ran ๐น โ { 0 } ) ( ๐ฅ ยท ( vol โ ( โก ๐น โ { ๐ฅ } ) ) ) ) |
2 |
|
i1frn |
โข ( ๐น โ dom โซ1 โ ran ๐น โ Fin ) |
3 |
|
difss |
โข ( ran ๐น โ { 0 } ) โ ran ๐น |
4 |
|
ssfi |
โข ( ( ran ๐น โ Fin โง ( ran ๐น โ { 0 } ) โ ran ๐น ) โ ( ran ๐น โ { 0 } ) โ Fin ) |
5 |
2 3 4
|
sylancl |
โข ( ๐น โ dom โซ1 โ ( ran ๐น โ { 0 } ) โ Fin ) |
6 |
|
i1ff |
โข ( ๐น โ dom โซ1 โ ๐น : โ โถ โ ) |
7 |
6
|
frnd |
โข ( ๐น โ dom โซ1 โ ran ๐น โ โ ) |
8 |
7
|
ssdifssd |
โข ( ๐น โ dom โซ1 โ ( ran ๐น โ { 0 } ) โ โ ) |
9 |
8
|
sselda |
โข ( ( ๐น โ dom โซ1 โง ๐ฅ โ ( ran ๐น โ { 0 } ) ) โ ๐ฅ โ โ ) |
10 |
|
i1fima2sn |
โข ( ( ๐น โ dom โซ1 โง ๐ฅ โ ( ran ๐น โ { 0 } ) ) โ ( vol โ ( โก ๐น โ { ๐ฅ } ) ) โ โ ) |
11 |
9 10
|
remulcld |
โข ( ( ๐น โ dom โซ1 โง ๐ฅ โ ( ran ๐น โ { 0 } ) ) โ ( ๐ฅ ยท ( vol โ ( โก ๐น โ { ๐ฅ } ) ) ) โ โ ) |
12 |
5 11
|
fsumrecl |
โข ( ๐น โ dom โซ1 โ ฮฃ ๐ฅ โ ( ran ๐น โ { 0 } ) ( ๐ฅ ยท ( vol โ ( โก ๐น โ { ๐ฅ } ) ) ) โ โ ) |
13 |
1 12
|
eqeltrd |
โข ( ๐น โ dom โซ1 โ ( โซ1 โ ๐น ) โ โ ) |