| Step | Hyp | Ref
| Expression |
|---|
| 1 | | measdivcst 33896 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π
βf/c /π (πββͺ π)) β (measuresβπ)) |
| 2 | | measfn 33876 |
. . . . . . . 8
β’ (π β (measuresβπ) β π Fn π) |
| 3 | 2 | adantr 479 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β π Fn π) |
| 4 | | measbase 33869 |
. . . . . . . 8
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
| 5 | 4 | adantr 479 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β π β βͺ ran sigAlgebra) |
| 6 | | simpr 483 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (πββͺ π)
β β+) |
| 7 | 3, 5, 6 | ofcfn 33772 |
. . . . . 6
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π
βf/c /π (πββͺ π)) Fn π) |
| 8 | 7 | fndmd 6654 |
. . . . 5
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β dom (π
βf/c /π (πββͺ π)) = π) |
| 9 | 8 | fveq2d 6894 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (measuresβdom (π βf/c /π
(πββͺ π)))
= (measuresβπ)) |
| 10 | 1, 9 | eleqtrrd 2828 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π
βf/c /π (πββͺ π)) β (measuresβdom
(π βf/c
/π (πββͺ π)))) |
| 11 | | measbasedom 33874 |
. . 3
β’ ((π βf/c
/π (πββͺ π)) β βͺ ran measures β (π βf/c /π
(πββͺ π))
β (measuresβdom (π βf/c /π
(πββͺ π)))) |
| 12 | 10, 11 | sylibr 233 |
. 2
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π
βf/c /π (πββͺ π)) β βͺ ran measures) |
| 13 | 8 | unieqd 4917 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β βͺ dom (π βf/c /π
(πββͺ π))
= βͺ π) |
| 14 | 13 | fveq2d 6894 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π
βf/c /π (πββͺ π))ββͺ dom (π βf/c /π
(πββͺ π)))
= ((π βf/c
/π (πββͺ π))ββͺ π)) |
| 15 | | unielsiga 33800 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β βͺ π β π) |
| 16 | 5, 15 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β βͺ π β π) |
| 17 | | eqidd 2726 |
. . . . 5
β’ (((π β (measuresβπ) β§ (πββͺ π) β β+)
β§ βͺ π β π) β (πββͺ π) = (πββͺ π)) |
| 18 | 3, 5, 6, 17 | ofcval 33771 |
. . . 4
β’ (((π β (measuresβπ) β§ (πββͺ π) β β+)
β§ βͺ π β π) β ((π βf/c /π
(πββͺ π))ββͺ π) = ((πββͺ π) /π (πββͺ π))) |
| 19 | 16, 18 | mpdan 685 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π
βf/c /π (πββͺ π))ββͺ π) =
((πββͺ π)
/π (πββͺ π))) |
| 20 | | rpre 13009 |
. . . . 5
β’ ((πββͺ π)
β β+ β (πββͺ π) β
β) |
| 21 | | rpne0 13017 |
. . . . 5
β’ ((πββͺ π)
β β+ β (πββͺ π) β 0) |
| 22 | | xdivid 32691 |
. . . . 5
β’ (((πββͺ π)
β β β§ (πββͺ π) β 0) β ((πββͺ π)
/π (πββͺ π)) = 1) |
| 23 | 20, 21, 22 | syl2anc 582 |
. . . 4
β’ ((πββͺ π)
β β+ β ((πββͺ π) /π (πββͺ π))
= 1) |
| 24 | 23 | adantl 480 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((πββͺ π)
/π (πββͺ π)) = 1) |
| 25 | 14, 19, 24 | 3eqtrd 2769 |
. 2
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π
βf/c /π (πββͺ π))ββͺ dom (π βf/c /π
(πββͺ π)))
= 1) |
| 26 | | elprob 34082 |
. 2
β’ ((π βf/c
/π (πββͺ π)) β Prob β ((π βf/c
/π (πββͺ π)) β βͺ ran measures β§ ((π βf/c /π
(πββͺ π))ββͺ dom
(π βf/c
/π (πββͺ π))) = 1)) |
| 27 | 12, 25, 26 | sylanbrc 581 |
1
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π
βf/c /π (πββͺ π)) β Prob) |
