Step | Hyp | Ref
| Expression |
1 | | 1xr 11221 |
. . . . . 6
β’ 1 β
β* |
2 | | 0le1 11685 |
. . . . . 6
β’ 0 β€
1 |
3 | | pnfge 13058 |
. . . . . . 7
β’ (1 β
β* β 1 β€ +β) |
4 | 1, 3 | ax-mp 5 |
. . . . . 6
β’ 1 β€
+β |
5 | | 0xr 11209 |
. . . . . . 7
β’ 0 β
β* |
6 | | pnfxr 11216 |
. . . . . . 7
β’ +β
β β* |
7 | | elicc1 13315 |
. . . . . . 7
β’ ((0
β β* β§ +β β β*) β (1
β (0[,]+β) β (1 β β* β§ 0 β€ 1 β§
1 β€ +β))) |
8 | 5, 6, 7 | mp2an 691 |
. . . . . 6
β’ (1 β
(0[,]+β) β (1 β β* β§ 0 β€ 1 β§ 1 β€
+β)) |
9 | 1, 2, 4, 8 | mpbir3an 1342 |
. . . . 5
β’ 1 β
(0[,]+β) |
10 | | 0e0iccpnf 13383 |
. . . . 5
β’ 0 β
(0[,]+β) |
11 | 9, 10 | ifcli 4538 |
. . . 4
β’ if(0
β π, 1, 0) β
(0[,]+β) |
12 | 11 | rgenw 3069 |
. . 3
β’
βπ β
π« βif(0 β π, 1, 0) β
(0[,]+β) |
13 | | df-dde 32872 |
. . . 4
β’ Ξ΄ =
(π β π« β
β¦ if(0 β π, 1,
0)) |
14 | 13 | fmpt 7063 |
. . 3
β’
(βπ β
π« βif(0 β π, 1, 0) β (0[,]+β) β
Ξ΄:π« ββΆ(0[,]+β)) |
15 | 12, 14 | mpbi 229 |
. 2
β’
Ξ΄:π« ββΆ(0[,]+β) |
16 | | 0ss 4361 |
. . 3
β’ β
β β |
17 | | noel 4295 |
. . 3
β’ Β¬ 0
β β
|
18 | | ddeval0 32874 |
. . 3
β’ ((β
β β β§ Β¬ 0 β β
) β (Ξ΄ββ
) =
0) |
19 | 16, 17, 18 | mp2an 691 |
. 2
β’
(Ξ΄ββ
) = 0 |
20 | | rabxm 4351 |
. . . . . . . . 9
β’ π₯ = ({π β π₯ β£ 0 β π} βͺ {π β π₯ β£ Β¬ 0 β π}) |
21 | | esumeq1 32673 |
. . . . . . . . 9
β’ (π₯ = ({π β π₯ β£ 0 β π} βͺ {π β π₯ β£ Β¬ 0 β π}) β Ξ£*π¦ β π₯(Ξ΄βπ¦) = Ξ£*π¦ β ({π β π₯ β£ 0 β π} βͺ {π β π₯ β£ Β¬ 0 β π})(Ξ΄βπ¦)) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
β’
Ξ£*π¦
β π₯(Ξ΄βπ¦) = Ξ£*π¦ β ({π β π₯ β£ 0 β π} βͺ {π β π₯ β£ Β¬ 0 β π})(Ξ΄βπ¦) |
23 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦ π₯ β π« π«
β |
24 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π¦{π β π₯ β£ 0 β π} |
25 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π¦{π β π₯ β£ Β¬ 0 β π} |
26 | | rabexg 5293 |
. . . . . . . . 9
β’ (π₯ β π« π«
β β {π β
π₯ β£ 0 β π} β V) |
27 | | rabexg 5293 |
. . . . . . . . 9
β’ (π₯ β π« π«
β β {π β
π₯ β£ Β¬ 0 β
π} β
V) |
28 | | rabnc 4352 |
. . . . . . . . . 10
β’ ({π β π₯ β£ 0 β π} β© {π β π₯ β£ Β¬ 0 β π}) = β
|
29 | 28 | a1i 11 |
. . . . . . . . 9
β’ (π₯ β π« π«
β β ({π β
π₯ β£ 0 β π} β© {π β π₯ β£ Β¬ 0 β π}) = β
) |
30 | | elrabi 3644 |
. . . . . . . . . . . 12
β’ (π¦ β {π β π₯ β£ 0 β π} β π¦ β π₯) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ 0 β π}) β π¦ β π₯) |
32 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ 0 β π}) β π₯ β π« π«
β) |
33 | | elelpwi 4575 |
. . . . . . . . . . 11
β’ ((π¦ β π₯ β§ π₯ β π« π« β) β
π¦ β π«
β) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ 0 β π}) β π¦ β π« β) |
35 | 15 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ (π¦ β π« β β
(Ξ΄βπ¦) β
(0[,]+β)) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ 0 β π}) β (Ξ΄βπ¦) β
(0[,]+β)) |
37 | | elrabi 3644 |
. . . . . . . . . . . 12
β’ (π¦ β {π β π₯ β£ Β¬ 0 β π} β π¦ β π₯) |
38 | 37 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β π¦ β π₯) |
39 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β π₯ β π« π«
β) |
40 | 38, 39, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β π¦ β π« β) |
41 | 40, 35 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β (Ξ΄βπ¦) β
(0[,]+β)) |
42 | 23, 24, 25, 26, 27, 29, 36, 41 | esumsplit 32692 |
. . . . . . . 8
β’ (π₯ β π« π«
β β Ξ£*π¦ β ({π β π₯ β£ 0 β π} βͺ {π β π₯ β£ Β¬ 0 β π})(Ξ΄βπ¦) = (Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) +π
Ξ£*π¦ β
{π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦))) |
43 | 22, 42 | eqtrid 2789 |
. . . . . . 7
β’ (π₯ β π« π«
β β Ξ£*π¦ β π₯(Ξ΄βπ¦) = (Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) +π
Ξ£*π¦ β
{π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦))) |
44 | 43 | adantr 482 |
. . . . . 6
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β Ξ£*π¦ β π₯(Ξ΄βπ¦) = (Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) +π
Ξ£*π¦ β
{π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦))) |
45 | | esumeq1 32673 |
. . . . . . . . . . . 12
β’ ({π β π₯ β£ 0 β π} = {π} β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = Ξ£*π¦ β {π} (Ξ΄βπ¦)) |
46 | 45 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = Ξ£*π¦ β {π} (Ξ΄βπ¦)) |
47 | | simp-4l 782 |
. . . . . . . . . . . 12
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β π₯ β π« π«
β) |
48 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π β V |
49 | 48 | rabsnel 31470 |
. . . . . . . . . . . . 13
β’ ({π β π₯ β£ 0 β π} = {π} β π β π₯) |
50 | 49 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β π β π₯) |
51 | | eleq2w 2822 |
. . . . . . . . . . . . . 14
β’ (π = π β (0 β π β 0 β π)) |
52 | 48, 51 | rabsnt 4697 |
. . . . . . . . . . . . 13
β’ ({π β π₯ β£ 0 β π} = {π} β 0 β π) |
53 | 52 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β 0 β π) |
54 | | elelpwi 4575 |
. . . . . . . . . . . . . . . 16
β’ ((π β π₯ β§ π₯ β π« π« β) β
π β π«
β) |
55 | 54 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π« π«
β β§ π β
π₯) β π β π«
β) |
56 | 55 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β π β π« β) |
57 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β π« β β§
π¦ = π) β π¦ = π) |
58 | 57 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ ((π β π« β β§
π¦ = π) β (Ξ΄βπ¦) = (Ξ΄βπ)) |
59 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β π« β β
π β
V) |
60 | 15 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . 15
β’ (π β π« β β
(Ξ΄βπ) β
(0[,]+β)) |
61 | 58, 59, 60 | esumsn 32704 |
. . . . . . . . . . . . . 14
β’ (π β π« β β
Ξ£*π¦ β
{π} (Ξ΄βπ¦) = (Ξ΄βπ)) |
62 | 56, 61 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β
Ξ£*π¦ β
{π} (Ξ΄βπ¦) = (Ξ΄βπ)) |
63 | 56 | elpwid 4574 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β π β β) |
64 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β 0 β π) |
65 | | ddeval1 32873 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 0 β
π) β
(Ξ΄βπ) =
1) |
66 | 63, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β (Ξ΄βπ) = 1) |
67 | 62, 66 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π₯ β π« π«
β β§ (π β
π₯ β§ 0 β π)) β
Ξ£*π¦ β
{π} (Ξ΄βπ¦) = 1) |
68 | 47, 50, 53, 67 | syl12anc 836 |
. . . . . . . . . . 11
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β Ξ£*π¦ β {π} (Ξ΄βπ¦) = 1) |
69 | 46, 68 | eqtrd 2777 |
. . . . . . . . . 10
β’
(((((π₯ β
π« π« β β§ Disj π¦ β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β§ π β π₯) β§ {π β π₯ β£ 0 β π} = {π}) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = 1) |
70 | | df-disj 5076 |
. . . . . . . . . . . . . . 15
β’
(Disj π¦
β π₯ π¦ β βπβ*π¦ β π₯ π β π¦) |
71 | | c0ex 11156 |
. . . . . . . . . . . . . . . 16
β’ 0 β
V |
72 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π β π¦ β 0 β π¦)) |
73 | 72 | rmobidv 3373 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (β*π¦ β π₯ π β π¦ β β*π¦ β π₯ 0 β π¦)) |
74 | 71, 73 | spcv 3567 |
. . . . . . . . . . . . . . 15
β’
(βπβ*π¦ β π₯ π β π¦ β β*π¦ β π₯ 0 β π¦) |
75 | 70, 74 | sylbi 216 |
. . . . . . . . . . . . . 14
β’
(Disj π¦
β π₯ π¦ β β*π¦ β π₯ 0 β π¦) |
76 | | rmo5 3376 |
. . . . . . . . . . . . . . . 16
β’
(β*π¦ β
π₯ 0 β π¦ β (βπ¦ β π₯ 0 β π¦ β β!π¦ β π₯ 0 β π¦)) |
77 | 76 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’
(β*π¦ β
π₯ 0 β π¦ β (βπ¦ β π₯ 0 β π¦ β β!π¦ β π₯ 0 β π¦)) |
78 | 77 | imp 408 |
. . . . . . . . . . . . . 14
β’
((β*π¦ β
π₯ 0 β π¦ β§ βπ¦ β π₯ 0 β π¦) β β!π¦ β π₯ 0 β π¦) |
79 | 75, 78 | sylan 581 |
. . . . . . . . . . . . 13
β’
((Disj π¦
β π₯ π¦ β§ βπ¦ β π₯ 0 β π¦) β β!π¦ β π₯ 0 β π¦) |
80 | | reusn 4693 |
. . . . . . . . . . . . 13
β’
(β!π¦ β
π₯ 0 β π¦ β βπ{π¦ β π₯ β£ 0 β π¦} = {π}) |
81 | 79, 80 | sylib 217 |
. . . . . . . . . . . 12
β’
((Disj π¦
β π₯ π¦ β§ βπ¦ β π₯ 0 β π¦) β βπ{π¦ β π₯ β£ 0 β π¦} = {π}) |
82 | | eleq2w 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = π¦ β (0 β π β 0 β π¦)) |
83 | 82 | cbvrabv 3420 |
. . . . . . . . . . . . . . . 16
β’ {π β π₯ β£ 0 β π} = {π¦ β π₯ β£ 0 β π¦} |
84 | 83 | eqeq1i 2742 |
. . . . . . . . . . . . . . 15
β’ ({π β π₯ β£ 0 β π} = {π} β {π¦ β π₯ β£ 0 β π¦} = {π}) |
85 | 49 | ancri 551 |
. . . . . . . . . . . . . . 15
β’ ({π β π₯ β£ 0 β π} = {π} β (π β π₯ β§ {π β π₯ β£ 0 β π} = {π})) |
86 | 84, 85 | sylbir 234 |
. . . . . . . . . . . . . 14
β’ ({π¦ β π₯ β£ 0 β π¦} = {π} β (π β π₯ β§ {π β π₯ β£ 0 β π} = {π})) |
87 | 86 | eximi 1838 |
. . . . . . . . . . . . 13
β’
(βπ{π¦ β π₯ β£ 0 β π¦} = {π} β βπ(π β π₯ β§ {π β π₯ β£ 0 β π} = {π})) |
88 | | df-rex 3075 |
. . . . . . . . . . . . 13
β’
(βπ β
π₯ {π β π₯ β£ 0 β π} = {π} β βπ(π β π₯ β§ {π β π₯ β£ 0 β π} = {π})) |
89 | 87, 88 | sylibr 233 |
. . . . . . . . . . . 12
β’
(βπ{π¦ β π₯ β£ 0 β π¦} = {π} β βπ β π₯ {π β π₯ β£ 0 β π} = {π}) |
90 | 81, 89 | syl 17 |
. . . . . . . . . . 11
β’
((Disj π¦
β π₯ π¦ β§ βπ¦ β π₯ 0 β π¦) β βπ β π₯ {π β π₯ β£ 0 β π} = {π}) |
91 | 90 | adantll 713 |
. . . . . . . . . 10
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β βπ β π₯ {π β π₯ β£ 0 β π} = {π}) |
92 | 69, 91 | r19.29a 3160 |
. . . . . . . . 9
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = 1) |
93 | | elpwi 4572 |
. . . . . . . . . . . 12
β’ (π₯ β π« π«
β β π₯ β
π« β) |
94 | | sspwuni 5065 |
. . . . . . . . . . . 12
β’ (π₯ β π« β
β βͺ π₯ β β) |
95 | 93, 94 | sylib 217 |
. . . . . . . . . . 11
β’ (π₯ β π« π«
β β βͺ π₯ β β) |
96 | | eluni2 4874 |
. . . . . . . . . . . 12
β’ (0 β
βͺ π₯ β βπ¦ β π₯ 0 β π¦) |
97 | 96 | biimpri 227 |
. . . . . . . . . . 11
β’
(βπ¦ β
π₯ 0 β π¦ β 0 β βͺ π₯) |
98 | | ddeval1 32873 |
. . . . . . . . . . 11
β’ ((βͺ π₯
β β β§ 0 β βͺ π₯) β (Ξ΄ββͺ π₯) =
1) |
99 | 95, 97, 98 | syl2an 597 |
. . . . . . . . . 10
β’ ((π₯ β π« π«
β β§ βπ¦
β π₯ 0 β π¦) β (Ξ΄ββͺ π₯) =
1) |
100 | 99 | adantlr 714 |
. . . . . . . . 9
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β (Ξ΄ββͺ π₯) =
1) |
101 | 92, 100 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ βπ¦ β π₯ 0 β π¦) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = (Ξ΄ββͺ π₯)) |
102 | | nfre1 3271 |
. . . . . . . . . . . . 13
β’
β²π¦βπ¦ β π₯ 0 β π¦ |
103 | 102 | nfn 1861 |
. . . . . . . . . . . 12
β’
β²π¦ Β¬
βπ¦ β π₯ 0 β π¦ |
104 | 82 | elrab 3650 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β {π β π₯ β£ 0 β π} β (π¦ β π₯ β§ 0 β π¦)) |
105 | 104 | exbii 1851 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ π¦ β {π β π₯ β£ 0 β π} β βπ¦(π¦ β π₯ β§ 0 β π¦)) |
106 | | neq0 4310 |
. . . . . . . . . . . . . . 15
β’ (Β¬
{π β π₯ β£ 0 β π} = β
β βπ¦ π¦ β {π β π₯ β£ 0 β π}) |
107 | | df-rex 3075 |
. . . . . . . . . . . . . . 15
β’
(βπ¦ β
π₯ 0 β π¦ β βπ¦(π¦ β π₯ β§ 0 β π¦)) |
108 | 105, 106,
107 | 3bitr4i 303 |
. . . . . . . . . . . . . 14
β’ (Β¬
{π β π₯ β£ 0 β π} = β
β βπ¦ β π₯ 0 β π¦) |
109 | 108 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (Β¬
{π β π₯ β£ 0 β π} = β
β βπ¦ β π₯ 0 β π¦) |
110 | 109 | con1i 147 |
. . . . . . . . . . . 12
β’ (Β¬
βπ¦ β π₯ 0 β π¦ β {π β π₯ β£ 0 β π} = β
) |
111 | 103, 110 | esumeq1d 32674 |
. . . . . . . . . . 11
β’ (Β¬
βπ¦ β π₯ 0 β π¦ β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = Ξ£*π¦ β β
(Ξ΄βπ¦)) |
112 | | esumnul 32687 |
. . . . . . . . . . 11
β’
Ξ£*π¦
β β
(Ξ΄βπ¦) = 0 |
113 | 111, 112 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (Β¬
βπ¦ β π₯ 0 β π¦ β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = 0) |
114 | 113 | adantl 483 |
. . . . . . . . 9
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ Β¬ βπ¦ β π₯ 0 β π¦) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = 0) |
115 | 96 | biimpi 215 |
. . . . . . . . . . . 12
β’ (0 β
βͺ π₯ β βπ¦ β π₯ 0 β π¦) |
116 | 115 | con3i 154 |
. . . . . . . . . . 11
β’ (Β¬
βπ¦ β π₯ 0 β π¦ β Β¬ 0 β βͺ π₯) |
117 | | ddeval0 32874 |
. . . . . . . . . . 11
β’ ((βͺ π₯
β β β§ Β¬ 0 β βͺ π₯) β (Ξ΄ββͺ π₯) =
0) |
118 | 95, 116, 117 | syl2an 597 |
. . . . . . . . . 10
β’ ((π₯ β π« π«
β β§ Β¬ βπ¦ β π₯ 0 β π¦) β (Ξ΄ββͺ π₯) =
0) |
119 | 118 | adantlr 714 |
. . . . . . . . 9
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ Β¬ βπ¦ β π₯ 0 β π¦) β (Ξ΄ββͺ π₯) =
0) |
120 | 114, 119 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β§ Β¬ βπ¦ β π₯ 0 β π¦) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = (Ξ΄ββͺ π₯)) |
121 | 101, 120 | pm2.61dan 812 |
. . . . . . 7
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) = (Ξ΄ββͺ π₯)) |
122 | 40 | elpwid 4574 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β π¦ β β) |
123 | 82 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β (Β¬ 0 β π β Β¬ 0 β π¦)) |
124 | 123 | elrab 3650 |
. . . . . . . . . . . . 13
β’ (π¦ β {π β π₯ β£ Β¬ 0 β π} β (π¦ β π₯ β§ Β¬ 0 β π¦)) |
125 | 124 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π¦ β {π β π₯ β£ Β¬ 0 β π} β Β¬ 0 β π¦) |
126 | 125 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β Β¬ 0 β π¦) |
127 | | ddeval0 32874 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ Β¬ 0
β π¦) β
(Ξ΄βπ¦) =
0) |
128 | 122, 126,
127 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π₯ β π« π«
β β§ π¦ β
{π β π₯ β£ Β¬ 0 β π}) β (Ξ΄βπ¦) = 0) |
129 | 128 | esumeq2dv 32677 |
. . . . . . . . 9
β’ (π₯ β π« π«
β β Ξ£*π¦ β {π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦) = Ξ£*π¦ β {π β π₯ β£ Β¬ 0 β π}0) |
130 | | vex 3452 |
. . . . . . . . . . 11
β’ π₯ β V |
131 | 130 | rabex 5294 |
. . . . . . . . . 10
β’ {π β π₯ β£ Β¬ 0 β π} β V |
132 | 25 | esum0 32688 |
. . . . . . . . . 10
β’ ({π β π₯ β£ Β¬ 0 β π} β V β Ξ£*π¦ β {π β π₯ β£ Β¬ 0 β π}0 = 0) |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . 9
β’
Ξ£*π¦
β {π β π₯ β£ Β¬ 0 β π}0 = 0 |
134 | 129, 133 | eqtrdi 2793 |
. . . . . . . 8
β’ (π₯ β π« π«
β β Ξ£*π¦ β {π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦) = 0) |
135 | 134 | adantr 482 |
. . . . . . 7
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β Ξ£*π¦ β {π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦) = 0) |
136 | 121, 135 | oveq12d 7380 |
. . . . . 6
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β (Ξ£*π¦ β {π β π₯ β£ 0 β π} (Ξ΄βπ¦) +π
Ξ£*π¦ β
{π β π₯ β£ Β¬ 0 β π} (Ξ΄βπ¦)) = ((Ξ΄ββͺ π₯)
+π 0)) |
137 | | vuniex 7681 |
. . . . . . . . . 10
β’ βͺ π₯
β V |
138 | 137 | elpw 4569 |
. . . . . . . . 9
β’ (βͺ π₯
β π« β β βͺ π₯ β β) |
139 | 138 | biimpri 227 |
. . . . . . . 8
β’ (βͺ π₯
β β β βͺ π₯ β π« β) |
140 | | iccssxr 13354 |
. . . . . . . . 9
β’
(0[,]+β) β β* |
141 | 15 | ffvelcdmi 7039 |
. . . . . . . . 9
β’ (βͺ π₯
β π« β β (Ξ΄ββͺ
π₯) β
(0[,]+β)) |
142 | 140, 141 | sselid 3947 |
. . . . . . . 8
β’ (βͺ π₯
β π« β β (Ξ΄ββͺ
π₯) β
β*) |
143 | | xaddid1 13167 |
. . . . . . . 8
β’
((Ξ΄ββͺ π₯) β β* β
((Ξ΄ββͺ π₯) +π 0) =
(Ξ΄ββͺ π₯)) |
144 | 95, 139, 142, 143 | 4syl 19 |
. . . . . . 7
β’ (π₯ β π« π«
β β ((Ξ΄ββͺ π₯) +π 0) =
(Ξ΄ββͺ π₯)) |
145 | 144 | adantr 482 |
. . . . . 6
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β ((Ξ΄ββͺ π₯)
+π 0) = (Ξ΄ββͺ π₯)) |
146 | 44, 136, 145 | 3eqtrrd 2782 |
. . . . 5
β’ ((π₯ β π« π«
β β§ Disj π¦
β π₯ π¦) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦)) |
147 | 146 | adantrl 715 |
. . . 4
β’ ((π₯ β π« π«
β β§ (π₯ βΌ
Ο β§ Disj π¦
β π₯ π¦)) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦)) |
148 | 147 | ex 414 |
. . 3
β’ (π₯ β π« π«
β β ((π₯ βΌ
Ο β§ Disj π¦
β π₯ π¦) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦))) |
149 | 148 | rgen 3067 |
. 2
β’
βπ₯ β
π« π« β((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦)) |
150 | | reex 11149 |
. . . 4
β’ β
β V |
151 | | pwsiga 32769 |
. . . 4
β’ (β
β V β π« β β
(sigAlgebraββ)) |
152 | 150, 151 | ax-mp 5 |
. . 3
β’ π«
β β (sigAlgebraββ) |
153 | | elrnsiga 32765 |
. . 3
β’
(π« β β (sigAlgebraββ) β π«
β β βͺ ran sigAlgebra) |
154 | | ismeas 32838 |
. . 3
β’
(π« β β βͺ ran sigAlgebra
β (Ξ΄ β (measuresβπ« β) β
(Ξ΄:π« ββΆ(0[,]+β) β§ (Ξ΄ββ
)
= 0 β§ βπ₯ β
π« π« β((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦))))) |
155 | 152, 153,
154 | mp2b 10 |
. 2
β’ (Ξ΄
β (measuresβπ« β) β (Ξ΄:π«
ββΆ(0[,]+β) β§ (Ξ΄ββ
) = 0 β§
βπ₯ β π«
π« β((π₯
βΌ Ο β§ Disj π¦ β π₯ π¦) β (Ξ΄ββͺ π₯) =
Ξ£*π¦ β
π₯(Ξ΄βπ¦)))) |
156 | 15, 19, 149, 155 | mpbir3an 1342 |
1
β’ Ξ΄
β (measuresβπ« β) |