Step | Hyp | Ref
| Expression |
1 | | itg10a.1 |
. . 3
β’ (π β πΉ β dom
β«1) |
2 | | itg1val 25063 |
. . 3
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β
(β«1βπΉ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
4 | | i1ff 25056 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
5 | 1, 4 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
6 | 5 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ (π β πΉ Fn β) |
7 | 6 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (ran πΉ β {0})) β πΉ Fn β) |
8 | | fniniseg 7015 |
. . . . . . . . . . . . 13
β’ (πΉ Fn β β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (ran πΉ β {0})) β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
10 | | eldifsni 4755 |
. . . . . . . . . . . . . . 15
β’ (π β (ran πΉ β {0}) β π β 0) |
11 | 10 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β π β 0) |
12 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β π₯ β β) |
13 | | eldif 3925 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (β β π΄) β (π₯ β β β§ Β¬ π₯ β π΄)) |
14 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β§ π₯ β (β β π΄)) β (πΉβπ₯) = π) |
15 | | itg10a.4 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (β β π΄)) β (πΉβπ₯) = 0) |
16 | 15 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β§ π₯ β (β β π΄)) β (πΉβπ₯) = 0) |
17 | 14, 16 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β§ π₯ β (β β π΄)) β π = 0) |
18 | 17 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (π₯ β (β β π΄) β π = 0)) |
19 | 13, 18 | biimtrrid 242 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β ((π₯ β β β§ Β¬ π₯ β π΄) β π = 0)) |
20 | 12, 19 | mpand 694 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (Β¬ π₯ β π΄ β π = 0)) |
21 | 20 | necon1ad 2961 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β (π β 0 β π₯ β π΄)) |
22 | 11, 21 | mpd 15 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (ran πΉ β {0})) β§ (π₯ β β β§ (πΉβπ₯) = π)) β π₯ β π΄) |
23 | 22 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β§ π β (ran πΉ β {0})) β ((π₯ β β β§ (πΉβπ₯) = π) β π₯ β π΄)) |
24 | 9, 23 | sylbid 239 |
. . . . . . . . . . 11
β’ ((π β§ π β (ran πΉ β {0})) β (π₯ β (β‘πΉ β {π}) β π₯ β π΄)) |
25 | 24 | ssrdv 3955 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) β π΄) |
26 | | itg10a.2 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β π΄ β β) |
28 | 25, 27 | sstrd 3959 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) β β) |
29 | | itg10a.3 |
. . . . . . . . . . 11
β’ (π β (vol*βπ΄) = 0) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β (vol*βπ΄) = 0) |
31 | | ovolssnul 24867 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π}) β π΄ β§ π΄ β β β§ (vol*βπ΄) = 0) β (vol*β(β‘πΉ β {π})) = 0) |
32 | 25, 27, 30, 31 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β (vol*β(β‘πΉ β {π})) = 0) |
33 | | nulmbl 24915 |
. . . . . . . . 9
β’ (((β‘πΉ β {π}) β β β§ (vol*β(β‘πΉ β {π})) = 0) β (β‘πΉ β {π}) β dom vol) |
34 | 28, 32, 33 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) β dom vol) |
35 | | mblvol 24910 |
. . . . . . . 8
β’ ((β‘πΉ β {π}) β dom vol β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
36 | 34, 35 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
37 | 36, 32 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) = 0) |
38 | 37 | oveq2d 7378 |
. . . . 5
β’ ((π β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΉ β {π}))) = (π Β· 0)) |
39 | 5 | frnd 6681 |
. . . . . . . . 9
β’ (π β ran πΉ β β) |
40 | 39 | ssdifssd 4107 |
. . . . . . . 8
β’ (π β (ran πΉ β {0}) β
β) |
41 | 40 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
42 | 41 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
43 | 42 | mul01d 11361 |
. . . . 5
β’ ((π β§ π β (ran πΉ β {0})) β (π Β· 0) = 0) |
44 | 38, 43 | eqtrd 2777 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΉ β {π}))) = 0) |
45 | 44 | sumeq2dv 15595 |
. . 3
β’ (π β Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π}))) = Ξ£π β (ran πΉ β {0})0) |
46 | | i1frn 25057 |
. . . . . . 7
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
47 | 1, 46 | syl 17 |
. . . . . 6
β’ (π β ran πΉ β Fin) |
48 | | difss 4096 |
. . . . . 6
β’ (ran
πΉ β {0}) β ran
πΉ |
49 | | ssfi 9124 |
. . . . . 6
β’ ((ran
πΉ β Fin β§ (ran
πΉ β {0}) β ran
πΉ) β (ran πΉ β {0}) β
Fin) |
50 | 47, 48, 49 | sylancl 587 |
. . . . 5
β’ (π β (ran πΉ β {0}) β Fin) |
51 | 50 | olcd 873 |
. . . 4
β’ (π β ((ran πΉ β {0}) β
(β€β₯β0) β¨ (ran πΉ β {0}) β Fin)) |
52 | | sumz 15614 |
. . . 4
β’ (((ran
πΉ β {0}) β
(β€β₯β0) β¨ (ran πΉ β {0}) β Fin) β
Ξ£π β (ran πΉ β {0})0 =
0) |
53 | 51, 52 | syl 17 |
. . 3
β’ (π β Ξ£π β (ran πΉ β {0})0 = 0) |
54 | 45, 53 | eqtrd 2777 |
. 2
β’ (π β Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π}))) = 0) |
55 | 3, 54 | eqtrd 2777 |
1
β’ (π β
(β«1βπΉ)
= 0) |