Step | Hyp | Ref
| Expression |
1 | | omsmeas.o |
. . . . . 6
β’ (π β π β π) |
2 | | omsmeas.r |
. . . . . 6
β’ (π β π
:πβΆ(0[,]+β)) |
3 | | omsf 32953 |
. . . . . 6
β’ ((π β π β§ π
:πβΆ(0[,]+β)) β
(toOMeasβπ
):π«
βͺ dom π
βΆ(0[,]+β)) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . 5
β’ (π β (toOMeasβπ
):π« βͺ dom π
βΆ(0[,]+β)) |
5 | | omsmeas.m |
. . . . . . 7
β’ π = (toOMeasβπ
) |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π β π = (toOMeasβπ
)) |
7 | 2 | fdmd 6680 |
. . . . . . . . 9
β’ (π β dom π
= π) |
8 | 7 | eqcomd 2739 |
. . . . . . . 8
β’ (π β π = dom π
) |
9 | 8 | unieqd 4880 |
. . . . . . 7
β’ (π β βͺ π =
βͺ dom π
) |
10 | 9 | pweqd 4578 |
. . . . . 6
β’ (π β π« βͺ π =
π« βͺ dom π
) |
11 | 6, 10 | feq12d 6657 |
. . . . 5
β’ (π β (π:π« βͺ
πβΆ(0[,]+β)
β (toOMeasβπ
):π« βͺ dom
π
βΆ(0[,]+β))) |
12 | 4, 11 | mpbird 257 |
. . . 4
β’ (π β π:π« βͺ
πβΆ(0[,]+β)) |
13 | | omsmeas.s |
. . . . 5
β’ π = (toCaraSigaβπ) |
14 | 1 | uniexd 7680 |
. . . . . 6
β’ (π β βͺ π
β V) |
15 | 14, 12 | carsgcl 32961 |
. . . . 5
β’ (π β (toCaraSigaβπ) β π« βͺ π) |
16 | 13, 15 | eqsstrid 3993 |
. . . 4
β’ (π β π β π« βͺ π) |
17 | 12, 16 | fssresd 6710 |
. . 3
β’ (π β (π βΎ π):πβΆ(0[,]+β)) |
18 | | omsmeas.d |
. . . . . . . 8
β’ (π β β
β dom π
) |
19 | | omsmeas.0 |
. . . . . . . 8
β’ (π β (π
ββ
) = 0) |
20 | 5, 1, 2, 18, 19 | oms0 32954 |
. . . . . . 7
β’ (π β (πββ
) = 0) |
21 | 14, 12, 20 | 0elcarsg 32964 |
. . . . . 6
β’ (π β β
β
(toCaraSigaβπ)) |
22 | 21, 13 | eleqtrrdi 2845 |
. . . . 5
β’ (π β β
β π) |
23 | | fvres 6862 |
. . . . 5
β’ (β
β π β ((π βΎ π)ββ
) = (πββ
)) |
24 | 22, 23 | syl 17 |
. . . 4
β’ (π β ((π βΎ π)ββ
) = (πββ
)) |
25 | 24, 20 | eqtrd 2773 |
. . 3
β’ (π β ((π βΎ π)ββ
) = 0) |
26 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
27 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
28 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
29 | 26, 27, 28 | cbvdisj 5081 |
. . . . . . 7
β’
(Disj π
β π π β Disj π β π π) |
30 | 29 | anbi2i 624 |
. . . . . 6
β’ ((π βΌ Ο β§
Disj π β π π) β (π βΌ Ο β§ Disj π β π π)) |
31 | 1 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π) |
32 | 2 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π
:πβΆ(0[,]+β)) |
33 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π« π) |
34 | 33 | elpwid 4570 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π) |
35 | 16 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π« βͺ π) |
36 | 34, 35 | sstrd 3955 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π« βͺ π) |
37 | 36 | sselda 3945 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β π β π« βͺ π) |
38 | 37 | elpwid 4570 |
. . . . . . . . . 10
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β π β βͺ π) |
39 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π βΌ Ο) |
40 | 5, 31, 32, 38, 39 | omssubadd 32957 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (πββͺ
π β π π) β€ Ξ£*π β π(πβπ)) |
41 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β βͺ π β V) |
42 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π:π« βͺ
πβΆ(0[,]+β)) |
43 | 20 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (πββ
) = 0) |
44 | | uniiun 5019 |
. . . . . . . . . . . . . . . 16
β’ βͺ π₯ =
βͺ π¦ β π₯ π¦ |
45 | 44 | fveq2i 6846 |
. . . . . . . . . . . . . . 15
β’ (πββͺ π₯) =
(πββͺ π¦ β π₯ π¦) |
46 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β π β π) |
47 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β π
:πβΆ(0[,]+β)) |
48 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β§ π¦ β π₯) β π₯ β π« βͺ π) |
49 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β§ π¦ β π₯) β π¦ β π₯) |
50 | 48, 49 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β§ π¦ β π₯) β π¦ β π« βͺ π) |
51 | 50 | elpwid 4570 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β§ π¦ β π₯) β π¦ β βͺ π) |
52 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β π₯ βΌ
Ο) |
53 | 5, 46, 47, 51, 52 | omssubadd 32957 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β (πββͺ π¦ β π₯ π¦) β€ Ξ£*π¦ β π₯(πβπ¦)) |
54 | 45, 53 | eqbrtrid 5141 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β (πββͺ π₯)
β€ Ξ£*π¦
β π₯(πβπ¦)) |
55 | 54 | 3adant1r 1178 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β (πββͺ π₯)
β€ Ξ£*π¦
β π₯(πβπ¦)) |
56 | 55 | 3adant1r 1178 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π₯ βΌ Ο β§ π₯ β π« βͺ π)
β (πββͺ π₯)
β€ Ξ£*π¦
β π₯(πβπ¦)) |
57 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β π β π) |
58 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β π
:πβΆ(0[,]+β)) |
59 | | simp2 1138 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β π₯ β π¦) |
60 | | elpwi 4568 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π« βͺ π
β π¦ β βͺ π) |
61 | 60 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β π¦ β βͺ π) |
62 | 5, 57, 58, 59, 61 | omsmon 32955 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β (πβπ₯) β€ (πβπ¦)) |
63 | 62 | 3adant1r 1178 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β (πβπ₯) β€ (πβπ¦)) |
64 | 63 | 3adant1r 1178 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π₯ β π¦ β§ π¦ β π« βͺ π)
β (πβπ₯) β€ (πβπ¦)) |
65 | | elpwi 4568 |
. . . . . . . . . . . . . 14
β’ (π β π« π β π β π) |
66 | 65 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β π) |
67 | 66, 13 | sseqtrdi 3995 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β π β (toCaraSigaβπ)) |
68 | 41, 42, 43, 56, 64, 39, 67 | carsgclctun 32978 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β βͺ π β (toCaraSigaβπ)) |
69 | 68, 13 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β βͺ π β π) |
70 | | fvres 6862 |
. . . . . . . . . . 11
β’ (βͺ π
β π β ((π βΎ π)ββͺ π) = (πββͺ π)) |
71 | | uniiun 5019 |
. . . . . . . . . . . 12
β’ βͺ π =
βͺ π β π π |
72 | 71 | fveq2i 6846 |
. . . . . . . . . . 11
β’ (πββͺ π) =
(πββͺ π β π π) |
73 | 70, 72 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (βͺ π
β π β ((π βΎ π)ββͺ π) = (πββͺ
π β π π)) |
74 | 69, 73 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) = (πββͺ
π β π π)) |
75 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) |
76 | 66 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β π β π) |
77 | | fvres 6862 |
. . . . . . . . . . . 12
β’ (π β π β ((π βΎ π)βπ) = (πβπ)) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β ((π βΎ π)βπ) = (πβπ)) |
79 | 78 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β βπ β π ((π βΎ π)βπ) = (πβπ)) |
80 | 75, 79 | esumeq2d 32693 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π((π βΎ π)βπ) = Ξ£*π β π(πβπ)) |
81 | 40, 74, 80 | 3brtr4d 5138 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) β€ Ξ£*π β π((π βΎ π)βπ)) |
82 | | snex 5389 |
. . . . . . . . . . . . 13
β’ {β
}
β V |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β {β
} β
V) |
84 | 42 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β π:π« βͺ
πβΆ(0[,]+β)) |
85 | 84, 37 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β (πβπ) β (0[,]+β)) |
86 | | elsni 4604 |
. . . . . . . . . . . . . 14
β’ (π β {β
} β π = β
) |
87 | 86 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π β {β
} β (πβπ) = (πββ
)) |
88 | 87, 43 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β {β
}) β (πβπ) = 0) |
89 | 33, 83, 85, 88 | esumpad2 32712 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β (π β {β
})(πβπ) = Ξ£*π β π(πβπ)) |
90 | | neldifsnd 4754 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Β¬ β
β (π β
{β
})) |
91 | | difss 4092 |
. . . . . . . . . . . . . 14
β’ (π β {β
}) β
π |
92 | | ssdomg 8943 |
. . . . . . . . . . . . . 14
β’ (π β π« π β ((π β {β
}) β π β (π β {β
}) βΌ π)) |
93 | 33, 91, 92 | mpisyl 21 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (π β {β
}) βΌ π) |
94 | | domtr 8950 |
. . . . . . . . . . . . 13
β’ (((π β {β
}) βΌ
π β§ π βΌ Ο) β (π β {β
}) βΌ
Ο) |
95 | 93, 39, 94 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (π β {β
}) βΌ
Ο) |
96 | 67 | ssdifssd 4103 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (π β {β
}) β
(toCaraSigaβπ)) |
97 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Disj π β π π) |
98 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²π¦π |
99 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
β’
β²ππ¦ |
100 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π = π¦ β π = π¦) |
101 | 98, 99, 100 | cbvdisj 5081 |
. . . . . . . . . . . . . 14
β’
(Disj π
β π π β Disj π¦ β π π¦) |
102 | 97, 101 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Disj π¦ β π π¦) |
103 | | disjss1 5077 |
. . . . . . . . . . . . 13
β’ ((π β {β
}) β
π β (Disj π¦ β π π¦ β Disj π¦ β (π β {β
})π¦)) |
104 | 91, 102, 103 | mpsyl 68 |
. . . . . . . . . . . 12
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Disj π¦ β (π β {β
})π¦) |
105 | 41, 42, 43, 56, 90, 95, 96, 104, 64 | carsggect 32975 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β (π β {β
})(πβπ) β€ (πββͺ (π β
{β
}))) |
106 | 89, 105 | eqbrtrrd 5130 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π(πβπ) β€ (πββͺ (π β
{β
}))) |
107 | | unidif0 5316 |
. . . . . . . . . . 11
β’ βͺ (π
β {β
}) = βͺ π |
108 | 107 | fveq2i 6846 |
. . . . . . . . . 10
β’ (πββͺ (π
β {β
})) = (πββͺ π) |
109 | 106, 108 | breqtrdi 5147 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π(πβπ) β€ (πββͺ π)) |
110 | 69, 70 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) = (πββͺ π)) |
111 | 109, 80, 110 | 3brtr4d 5138 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π((π βΎ π)βπ) β€ ((π βΎ π)ββͺ π)) |
112 | 81, 111 | jca 513 |
. . . . . . 7
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (((π βΎ π)ββͺ π) β€ Ξ£*π β π((π βΎ π)βπ) β§ Ξ£*π β π((π βΎ π)βπ) β€ ((π βΎ π)ββͺ π))) |
113 | | iccssxr 13353 |
. . . . . . . . 9
β’
(0[,]+β) β β* |
114 | 17 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (π βΎ π):πβΆ(0[,]+β)) |
115 | 114, 69 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) β
(0[,]+β)) |
116 | 113, 115 | sselid 3943 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) β
β*) |
117 | 114 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β (π βΎ π):πβΆ(0[,]+β)) |
118 | 117, 76 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’ ((((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β§ π β π) β ((π βΎ π)βπ) β (0[,]+β)) |
119 | 118 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β βπ β π ((π βΎ π)βπ) β (0[,]+β)) |
120 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ |
121 | 120 | esumcl 32686 |
. . . . . . . . . 10
β’ ((π β π« π β§ βπ β π ((π βΎ π)βπ) β (0[,]+β)) β
Ξ£*π β
π((π βΎ π)βπ) β (0[,]+β)) |
122 | 33, 119, 121 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π((π βΎ π)βπ) β (0[,]+β)) |
123 | 113, 122 | sselid 3943 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β Ξ£*π β π((π βΎ π)βπ) β
β*) |
124 | | xrletri3 13079 |
. . . . . . . 8
β’ ((((π βΎ π)ββͺ π) β β*
β§ Ξ£*π
β π((π βΎ π)βπ) β β*) β (((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ) β (((π βΎ π)ββͺ π) β€ Ξ£*π β π((π βΎ π)βπ) β§ Ξ£*π β π((π βΎ π)βπ) β€ ((π βΎ π)ββͺ π)))) |
125 | 116, 123,
124 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β (((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ) β (((π βΎ π)ββͺ π) β€ Ξ£*π β π((π βΎ π)βπ) β§ Ξ£*π β π((π βΎ π)βπ) β€ ((π βΎ π)ββͺ π)))) |
126 | 112, 125 | mpbird 257 |
. . . . . 6
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ)) |
127 | 30, 126 | sylan2b 595 |
. . . . 5
β’ (((π β§ π β π« π) β§ (π βΌ Ο β§ Disj π β π π)) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ)) |
128 | 127 | ex 414 |
. . . 4
β’ ((π β§ π β π« π) β ((π βΌ Ο β§ Disj π β π π) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ))) |
129 | 128 | ralrimiva 3140 |
. . 3
β’ (π β βπ β π« π((π βΌ Ο β§ Disj π β π π) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ))) |
130 | 17, 25, 129 | 3jca 1129 |
. 2
β’ (π β ((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ β π« π((π βΌ Ο β§ Disj π β π π) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ)))) |
131 | 14, 12, 20, 54, 62 | carsgsiga 32979 |
. . . 4
β’ (π β (toCaraSigaβπ) β (sigAlgebraββͺ π)) |
132 | 13, 131 | eqeltrid 2838 |
. . 3
β’ (π β π β (sigAlgebraββͺ π)) |
133 | | elrnsiga 32782 |
. . 3
β’ (π β (sigAlgebraββͺ π)
β π β βͺ ran sigAlgebra) |
134 | | ismeas 32855 |
. . 3
β’ (π β βͺ ran sigAlgebra β ((π βΎ π) β (measuresβπ) β ((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ β π« π((π βΌ Ο β§ Disj π β π π) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ))))) |
135 | 132, 133,
134 | 3syl 18 |
. 2
β’ (π β ((π βΎ π) β (measuresβπ) β ((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ β π« π((π βΌ Ο β§ Disj π β π π) β ((π βΎ π)ββͺ π) = Ξ£*π β π((π βΎ π)βπ))))) |
136 | 130, 135 | mpbird 257 |
1
β’ (π β (π βΎ π) β (measuresβπ)) |