Step | Hyp | Ref
| Expression |
1 | | itg1val 25199 |
. . 3
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) |
2 | 1 | adantr 481 |
. 2
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
(β«1βπΉ)
= Ξ£π₯ β (ran
πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯})))) |
3 | | simpr2 1195 |
. . 3
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β (ran
πΉ β {0}) β
π΄) |
4 | 3 | sselda 3982 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (ran πΉ β {0})) β π₯ β π΄) |
5 | | simpr3 1196 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
π΄ β (β β
{0})) |
6 | 5 | sselda 3982 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β π₯ β (β β
{0})) |
7 | | eldifi 4126 |
. . . . . . 7
β’ (π₯ β (β β {0})
β π₯ β
β) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β π₯ β β) |
9 | | i1fima2sn 25196 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π₯ β (β
β {0})) β (volβ(β‘πΉ β {π₯})) β β) |
10 | 9 | adantlr 713 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (β β {0}))
β (volβ(β‘πΉ β {π₯})) β β) |
11 | 6, 10 | syldan 591 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (volβ(β‘πΉ β {π₯})) β β) |
12 | 8, 11 | remulcld 11243 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
13 | 12 | recnd 11241 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β π΄) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
14 | 4, 13 | syldan 591 |
. . 3
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (ran πΉ β {0})) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) β β) |
15 | | i1ff 25192 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
16 | 15 | ad2antrr 724 |
. . . . . . . . 9
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β πΉ:ββΆβ) |
17 | | ffrn 6731 |
. . . . . . . . 9
β’ (πΉ:ββΆβ β
πΉ:ββΆran πΉ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β πΉ:ββΆran πΉ) |
19 | | eldifn 4127 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β (ran πΉ β {0})) β Β¬ π₯ β (ran πΉ β {0})) |
20 | 19 | adantl 482 |
. . . . . . . . . 10
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β (ran πΉ β {0})) |
21 | | eldif 3958 |
. . . . . . . . . . 11
β’ (π₯ β (ran πΉ β {0}) β (π₯ β ran πΉ β§ Β¬ π₯ β {0})) |
22 | | simplr3 1217 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π΄ β (β β
{0})) |
23 | 22 | ssdifssd 4142 |
. . . . . . . . . . . . . 14
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π΄ β (ran πΉ β {0})) β (β β
{0})) |
24 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β (π΄ β (ran πΉ β {0}))) |
25 | 23, 24 | sseldd 3983 |
. . . . . . . . . . . . 13
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β (β β
{0})) |
26 | | eldifn 4127 |
. . . . . . . . . . . . 13
β’ (π₯ β (β β {0})
β Β¬ π₯ β
{0}) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β {0}) |
28 | 27 | biantrud 532 |
. . . . . . . . . . 11
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ β ran πΉ β (π₯ β ran πΉ β§ Β¬ π₯ β {0}))) |
29 | 21, 28 | bitr4id 289 |
. . . . . . . . . 10
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ β (ran πΉ β {0}) β π₯ β ran πΉ)) |
30 | 20, 29 | mtbid 323 |
. . . . . . . . 9
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β Β¬ π₯ β ran πΉ) |
31 | | disjsn 4715 |
. . . . . . . . 9
β’ ((ran
πΉ β© {π₯}) = β
β Β¬ π₯ β ran πΉ) |
32 | 30, 31 | sylibr 233 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (ran πΉ β© {π₯}) = β
) |
33 | | fimacnvdisj 6769 |
. . . . . . . 8
β’ ((πΉ:ββΆran πΉ β§ (ran πΉ β© {π₯}) = β
) β (β‘πΉ β {π₯}) = β
) |
34 | 18, 32, 33 | syl2anc 584 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (β‘πΉ β {π₯}) = β
) |
35 | 34 | fveq2d 6895 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (volβ(β‘πΉ β {π₯})) = (volββ
)) |
36 | | 0mbl 25055 |
. . . . . . . 8
β’ β
β dom vol |
37 | | mblvol 25046 |
. . . . . . . 8
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
β’
(volββ
) = (vol*ββ
) |
39 | | ovol0 25009 |
. . . . . . 7
β’
(vol*ββ
) = 0 |
40 | 38, 39 | eqtri 2760 |
. . . . . 6
β’
(volββ
) = 0 |
41 | 35, 40 | eqtrdi 2788 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (volβ(β‘πΉ β {π₯})) = 0) |
42 | 41 | oveq2d 7424 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) = (π₯ Β· 0)) |
43 | | eldifi 4126 |
. . . . . . 7
β’ (π₯ β (π΄ β (ran πΉ β {0})) β π₯ β π΄) |
44 | 43, 8 | sylan2 593 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β β) |
45 | 44 | recnd 11241 |
. . . . 5
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β π₯ β β) |
46 | 45 | mul01d 11412 |
. . . 4
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· 0) = 0) |
47 | 42, 46 | eqtrd 2772 |
. . 3
β’ (((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β§ π₯ β (π΄ β (ran πΉ β {0}))) β (π₯ Β· (volβ(β‘πΉ β {π₯}))) = 0) |
48 | | simpr1 1194 |
. . 3
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
π΄ β
Fin) |
49 | 3, 14, 47, 48 | fsumss 15670 |
. 2
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
Ξ£π₯ β (ran πΉ β {0})(π₯ Β· (volβ(β‘πΉ β {π₯}))) = Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) |
50 | 2, 49 | eqtrd 2772 |
1
β’ ((πΉ β dom β«1
β§ (π΄ β Fin β§
(ran πΉ β {0}) β
π΄ β§ π΄ β (β β {0}))) β
(β«1βπΉ)
= Ξ£π₯ β π΄ (π₯ Β· (volβ(β‘πΉ β {π₯})))) |