Step | Hyp | Ref
| Expression |
1 | | itg1val 25063 |
. . 3
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) |
2 | 1 | adantr 482 |
. 2
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
(β«1βπΉ)
= Ξ£π₯ β (ran
πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) |
3 | | simpr2 1196 |
. . 3
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β (ran
πΉ β {0}) β
π΄) |
4 | 3 | sselda 3949 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (ran πΉ β {0})) β π₯ β π΄) |
5 | | simpr3 1197 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
π΄ β (β β
{0})) |
6 | 5 | sselda 3949 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β π₯ β (β β
{0})) |
7 | | eldifi 4091 |
. . . . . . 7
β’ (π₯ β (β β {0})
β π₯ β
β) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β π₯ β β) |
9 | | i1fima2sn 25060 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π₯ β (β
β {0})) β (volβ(β‘πΉ β {π₯})) β β) |
10 | 9 | adantlr 714 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (β β {0}))
β (volβ(β‘πΉ β {π₯})) β β) |
11 | 6, 10 | syldan 592 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (volβ(β‘πΉ β {π₯})) β β) |
12 | 8, 11 | remulcld 11192 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
13 | 12 | recnd 11190 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
14 | 4, 13 | syldan 592 |
. . 3
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (ran πΉ β {0})) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
15 | | i1ff 25056 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
16 | 15 | ad2antrr 725 |
. . . . . . . . 9
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β πΉ:ββΆβ) |
17 | | ffrn 6687 |
. . . . . . . . 9
β’ (πΉ:ββΆβ β
πΉ:ββΆran πΉ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β πΉ:ββΆran πΉ) |
19 | | eldifn 4092 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β (ran πΉ β {0})) β Β¬ π₯ β (ran πΉ β {0})) |
20 | 19 | adantl 483 |
. . . . . . . . . 10
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β (ran πΉ β {0})) |
21 | | eldif 3925 |
. . . . . . . . . . 11
β’ (π₯ β (ran πΉ β {0}) β (π₯ β ran πΉ β§ Β¬ π₯ β {0})) |
22 | | simplr3 1218 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π΄ β (β β
{0})) |
23 | 22 | ssdifssd 4107 |
. . . . . . . . . . . . . 14
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π΄ β (ran πΉ β {0})) β (β β
{0})) |
24 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β (π΄ β (ran πΉ β {0}))) |
25 | 23, 24 | sseldd 3950 |
. . . . . . . . . . . . 13
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β (β β
{0})) |
26 | | eldifn 4092 |
. . . . . . . . . . . . 13
β’ (π₯ β (β β {0})
β Β¬ π₯ β
{0}) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β {0}) |
28 | 27 | biantrud 533 |
. . . . . . . . . . 11
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ β ran πΉ β (π₯ β ran πΉ β§ Β¬ π₯ β {0}))) |
29 | 21, 28 | bitr4id 290 |
. . . . . . . . . 10
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ β (ran πΉ β {0}) β π₯ β ran πΉ)) |
30 | 20, 29 | mtbid 324 |
. . . . . . . . 9
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β ran πΉ) |
31 | | disjsn 4677 |
. . . . . . . . 9
β’ ((ran
πΉ β© {π₯}) = β
β Β¬ π₯ β ran πΉ) |
32 | 30, 31 | sylibr 233 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (ran πΉ β© {π₯}) = β
) |
33 | | fimacnvdisj 6725 |
. . . . . . . 8
β’ ((πΉ:ββΆran πΉ β§ (ran πΉ β© {π₯}) = β
) β (β‘πΉ β {π₯}) = β
) |
34 | 18, 32, 33 | syl2anc 585 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (β‘πΉ β {π₯}) = β
) |
35 | 34 | fveq2d 6851 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (volβ(β‘πΉ β {π₯})) = (volββ
)) |
36 | | 0mbl 24919 |
. . . . . . . 8
β’ β
β dom vol |
37 | | mblvol 24910 |
. . . . . . . 8
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
β’
(volββ
) = (vol*ββ
) |
39 | | ovol0 24873 |
. . . . . . 7
β’
(vol*ββ
) = 0 |
40 | 38, 39 | eqtri 2765 |
. . . . . 6
β’
(volββ
) = 0 |
41 | 35, 40 | eqtrdi 2793 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (volβ(β‘πΉ β {π₯})) = 0) |
42 | 41 | oveq2d 7378 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) = (π₯ Β· 0)) |
43 | | eldifi 4091 |
. . . . . . 7
β’ (π₯ β (π΄ β (ran πΉ β {0})) β π₯ β π΄) |
44 | 43, 8 | sylan2 594 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β β) |
45 | 44 | recnd 11190 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β β) |
46 | 45 | mul01d 11361 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· 0) = 0) |
47 | 42, 46 | eqtrd 2777 |
. . 3
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) = 0) |
48 | | simpr1 1195 |
. . 3
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
π΄ β
Fin) |
49 | 3, 14, 47, 48 | fsumss 15617 |
. 2
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯}))) = Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) |
50 | 2, 49 | eqtrd 2777 |
1
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
(β«1βπΉ)
= Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) |