Step | Hyp | Ref
| Expression |
1 | | measdivcstALTV 32864 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β (measuresβπ)) |
2 | | ovex 7395 |
. . . . . . 7
β’ ((πβπ₯) /π (πββͺ π)) β V |
3 | 2 | rgenw 3069 |
. . . . . 6
β’
βπ₯ β
π ((πβπ₯) /π (πββͺ π)) β V |
4 | | dmmptg 6199 |
. . . . . 6
β’
(βπ₯ β
π ((πβπ₯) /π (πββͺ π)) β V β dom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) = π) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
β’ dom
(π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) = π |
6 | 5 | fveq2i 6850 |
. . . 4
β’
(measuresβdom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))) = (measuresβπ) |
7 | 1, 6 | eleqtrrdi 2849 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β (measuresβdom
(π₯ β π β¦ ((πβπ₯) /π (πββͺ π))))) |
8 | | measbasedom 32841 |
. . 3
β’ ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β βͺ ran measures β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β (measuresβdom
(π₯ β π β¦ ((πβπ₯) /π (πββͺ π))))) |
9 | 7, 8 | sylibr 233 |
. 2
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β βͺ ran measures) |
10 | 5 | unieqi 4883 |
. . . 4
β’ βͺ dom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) = βͺ π |
11 | 10 | fveq2i 6850 |
. . 3
β’ ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ dom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))) = ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ π) |
12 | | measbase 32836 |
. . . . . . 7
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
13 | | isrnsigau 32766 |
. . . . . . . . 9
β’ (π β βͺ ran sigAlgebra β (π β π« βͺ π
β§ (βͺ π β π β§ βπ¦ β π (βͺ π β π¦) β π β§ βπ¦ β π« π(π¦ βΌ Ο β βͺ π¦
β π)))) |
14 | 13 | simprd 497 |
. . . . . . . 8
β’ (π β βͺ ran sigAlgebra β (βͺ
π β π β§ βπ¦ β π (βͺ π β π¦) β π β§ βπ¦ β π« π(π¦ βΌ Ο β βͺ π¦
β π))) |
15 | 14 | simp1d 1143 |
. . . . . . 7
β’ (π β βͺ ran sigAlgebra β βͺ π β π) |
16 | 12, 15 | syl 17 |
. . . . . 6
β’ (π β (measuresβπ) β βͺ π
β π) |
17 | | id 22 |
. . . . . . 7
β’ ((πββͺ π)
β β+ β (πββͺ π) β
β+) |
18 | 17, 17 | rpxdivcld 31832 |
. . . . . 6
β’ ((πββͺ π)
β β+ β ((πββͺ π) /π (πββͺ π))
β β+) |
19 | 16, 18 | anim12i 614 |
. . . . 5
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (βͺ π β π β§ ((πββͺ π) /π (πββͺ π))
β β+)) |
20 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = βͺ
π β (πβπ₯) = (πββͺ π)) |
21 | 20 | oveq1d 7377 |
. . . . . 6
β’ (π₯ = βͺ
π β ((πβπ₯) /π (πββͺ π)) = ((πββͺ π) /π (πββͺ π))) |
22 | | eqid 2737 |
. . . . . 6
β’ (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) = (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) |
23 | 21, 22 | fvmptg 6951 |
. . . . 5
β’ ((βͺ π
β π β§ ((πββͺ π)
/π (πββͺ π)) β β+)
β ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ π) =
((πββͺ π)
/π (πββͺ π))) |
24 | 19, 23 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ π) =
((πββͺ π)
/π (πββͺ π))) |
25 | | rpre 12930 |
. . . . . 6
β’ ((πββͺ π)
β β+ β (πββͺ π) β
β) |
26 | | rpne0 12938 |
. . . . . 6
β’ ((πββͺ π)
β β+ β (πββͺ π) β 0) |
27 | | xdivid 31826 |
. . . . . 6
β’ (((πββͺ π)
β β β§ (πββͺ π) β 0) β ((πββͺ π)
/π (πββͺ π)) = 1) |
28 | 25, 26, 27 | syl2anc 585 |
. . . . 5
β’ ((πββͺ π)
β β+ β ((πββͺ π) /π (πββͺ π))
= 1) |
29 | 28 | adantl 483 |
. . . 4
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((πββͺ π)
/π (πββͺ π)) = 1) |
30 | 24, 29 | eqtrd 2777 |
. . 3
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ π) =
1) |
31 | 11, 30 | eqtrid 2789 |
. 2
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ dom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))) = 1) |
32 | | elprob 33049 |
. 2
β’ ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β Prob β ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β βͺ ran measures β§ ((π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))ββͺ dom (π₯ β π β¦ ((πβπ₯) /π (πββͺ π)))) = 1)) |
33 | 9, 31, 32 | sylanbrc 584 |
1
β’ ((π β (measuresβπ) β§ (πββͺ π) β β+)
β (π₯ β π β¦ ((πβπ₯) /π (πββͺ π))) β
Prob) |