Step | Hyp | Ref
| Expression |
1 | | df-ov 7412 |
. 2
β’ (π΄(cprobβπ)π΅) = ((cprobβπ)ββ¨π΄, π΅β©) |
2 | | df-cndprob 33431 |
. . . . 5
β’ cprob =
(π β Prob β¦
(π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) |
3 | | dmeq 5904 |
. . . . . 6
β’ (π = π β dom π = dom π) |
4 | | fveq1 6891 |
. . . . . . 7
β’ (π = π β (πβ(π β© π)) = (πβ(π β© π))) |
5 | | fveq1 6891 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
6 | 4, 5 | oveq12d 7427 |
. . . . . 6
β’ (π = π β ((πβ(π β© π)) / (πβπ)) = ((πβ(π β© π)) / (πβπ))) |
7 | 3, 3, 6 | mpoeq123dv 7484 |
. . . . 5
β’ (π = π β (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ))) = (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) |
8 | | id 22 |
. . . . 5
β’ (π β Prob β π β Prob) |
9 | | dmexg 7894 |
. . . . . 6
β’ (π β Prob β dom π β V) |
10 | | mpoexga 8064 |
. . . . . 6
β’ ((dom
π β V β§ dom π β V) β (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ))) β V) |
11 | 9, 9, 10 | syl2anc 585 |
. . . . 5
β’ (π β Prob β (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ))) β V) |
12 | 2, 7, 8, 11 | fvmptd3 7022 |
. . . 4
β’ (π β Prob β
(cprobβπ) = (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) |
13 | 12 | 3ad2ant1 1134 |
. . 3
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β (cprobβπ) = (π β dom π, π β dom π β¦ ((πβ(π β© π)) / (πβπ)))) |
14 | | simprl 770 |
. . . . . 6
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β π = π΄) |
15 | | simprr 772 |
. . . . . 6
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β π = π΅) |
16 | 14, 15 | ineq12d 4214 |
. . . . 5
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β (π β© π) = (π΄ β© π΅)) |
17 | 16 | fveq2d 6896 |
. . . 4
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β (πβ(π β© π)) = (πβ(π΄ β© π΅))) |
18 | 15 | fveq2d 6896 |
. . . 4
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β (πβπ) = (πβπ΅)) |
19 | 17, 18 | oveq12d 7427 |
. . 3
β’ (((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β§ (π = π΄ β§ π = π΅)) β ((πβ(π β© π)) / (πβπ)) = ((πβ(π΄ β© π΅)) / (πβπ΅))) |
20 | | simp2 1138 |
. . 3
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β π΄ β dom π) |
21 | | simp3 1139 |
. . 3
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β π΅ β dom π) |
22 | | ovexd 7444 |
. . 3
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β ((πβ(π΄ β© π΅)) / (πβπ΅)) β V) |
23 | 13, 19, 20, 21, 22 | ovmpod 7560 |
. 2
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β (π΄(cprobβπ)π΅) = ((πβ(π΄ β© π΅)) / (πβπ΅))) |
24 | 1, 23 | eqtr3id 2787 |
1
β’ ((π β Prob β§ π΄ β dom π β§ π΅ β dom π) β ((cprobβπ)ββ¨π΄, π΅β©) = ((πβ(π΄ β© π΅)) / (πβπ΅))) |