Step | Hyp | Ref
| Expression |
1 | | hoimbl.x |
. . . . 5
β’ (π β π β Fin) |
2 | 1 | adantr 481 |
. . . 4
β’ ((π β§ π = β
) β π β Fin) |
3 | 2 | rrnmbl 44756 |
. . 3
β’ ((π β§ π = β
) β (β
βm π)
β dom (volnβπ)) |
4 | | reex 11100 |
. . . . . . . . 9
β’ β
β V |
5 | | mapdm0 8738 |
. . . . . . . . 9
β’ (β
β V β (β βm β
) =
{β
}) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . 8
β’ (β
βm β
) = {β
} |
7 | 6 | eqcomi 2746 |
. . . . . . 7
β’ {β
}
= (β βm β
) |
8 | 7 | a1i 11 |
. . . . . 6
β’ (π = β
β {β
} =
(β βm β
)) |
9 | | id 22 |
. . . . . . . 8
β’ (π = β
β π = β
) |
10 | 9 | ixpeq1d 8805 |
. . . . . . 7
β’ (π = β
β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = Xπ β β
((π΄βπ)[,)(π΅βπ))) |
11 | | ixp0x 8822 |
. . . . . . . 8
β’ Xπ β
β
((π΄βπ)[,)(π΅βπ)) = {β
} |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π = β
β Xπ β
β
((π΄βπ)[,)(π΅βπ)) = {β
}) |
13 | 10, 12 | eqtrd 2777 |
. . . . . 6
β’ (π = β
β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = {β
}) |
14 | | oveq2 7359 |
. . . . . 6
β’ (π = β
β (β
βm π) =
(β βm β
)) |
15 | 8, 13, 14 | 3eqtr4d 2787 |
. . . . 5
β’ (π = β
β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = (β βm π)) |
16 | 15 | adantl 482 |
. . . 4
β’ ((π β§ π = β
) β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = (β βm π)) |
17 | | hoimbl.s |
. . . . 5
β’ π = dom (volnβπ) |
18 | 17 | a1i 11 |
. . . 4
β’ ((π β§ π = β
) β π = dom (volnβπ)) |
19 | 16, 18 | eleq12d 2832 |
. . 3
β’ ((π β§ π = β
) β (Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π β (β βm π) β dom (volnβπ))) |
20 | 3, 19 | mpbird 256 |
. 2
β’ ((π β§ π = β
) β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π) |
21 | 1 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β Fin) |
22 | 9 | necon3bi 2968 |
. . . 4
β’ (Β¬
π = β
β π β β
) |
23 | 22 | adantl 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β π β β
) |
24 | | hoimbl.a |
. . . 4
β’ (π β π΄:πβΆβ) |
25 | 24 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β π΄:πβΆβ) |
26 | | hoimbl.b |
. . . 4
β’ (π β π΅:πβΆβ) |
27 | 26 | adantr 481 |
. . 3
β’ ((π β§ Β¬ π = β
) β π΅:πβΆβ) |
28 | | id 22 |
. . . . . 6
β’ (π€ = π₯ β π€ = π₯) |
29 | | eqidd 2738 |
. . . . . 6
β’ (π€ = π₯ β β = β) |
30 | 28 | ixpeq1d 8805 |
. . . . . . 7
β’ (π€ = π₯ β Xπ β π€ if(π = β, (-β(,)π§), β) = Xπ β π₯ if(π = β, (-β(,)π§), β)) |
31 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π = π β (π = β β π = β)) |
32 | 31 | ifbid 4507 |
. . . . . . . . 9
β’ (π = π β if(π = β, (-β(,)π§), β) = if(π = β, (-β(,)π§), β)) |
33 | 32 | cbvixpv 8811 |
. . . . . . . 8
β’ Xπ β
π₯ if(π = β, (-β(,)π§), β) = Xπ β π₯ if(π = β, (-β(,)π§), β) |
34 | 33 | a1i 11 |
. . . . . . 7
β’ (π€ = π₯ β Xπ β π₯ if(π = β, (-β(,)π§), β) = Xπ β π₯ if(π = β, (-β(,)π§), β)) |
35 | 30, 34 | eqtrd 2777 |
. . . . . 6
β’ (π€ = π₯ β Xπ β π€ if(π = β, (-β(,)π§), β) = Xπ β π₯ if(π = β, (-β(,)π§), β)) |
36 | 28, 29, 35 | mpoeq123dv 7426 |
. . . . 5
β’ (π€ = π₯ β (β β π€, π§ β β β¦ Xπ β
π€ if(π = β, (-β(,)π§), β)) = (β β π₯, π§ β β β¦ Xπ β
π₯ if(π = β, (-β(,)π§), β))) |
37 | | eqeq2 2749 |
. . . . . . . . 9
β’ (β = π β (π = β β π = π)) |
38 | 37 | ifbid 4507 |
. . . . . . . 8
β’ (β = π β if(π = β, (-β(,)π§), β) = if(π = π, (-β(,)π§), β)) |
39 | 38 | ixpeq2dv 8809 |
. . . . . . 7
β’ (β = π β Xπ β π₯ if(π = β, (-β(,)π§), β) = Xπ β π₯ if(π = π, (-β(,)π§), β)) |
40 | | oveq2 7359 |
. . . . . . . . 9
β’ (π§ = π¦ β (-β(,)π§) = (-β(,)π¦)) |
41 | 40 | ifeq1d 4503 |
. . . . . . . 8
β’ (π§ = π¦ β if(π = π, (-β(,)π§), β) = if(π = π, (-β(,)π¦), β)) |
42 | 41 | ixpeq2dv 8809 |
. . . . . . 7
β’ (π§ = π¦ β Xπ β π₯ if(π = π, (-β(,)π§), β) = Xπ β π₯ if(π = π, (-β(,)π¦), β)) |
43 | 39, 42 | cbvmpov 7446 |
. . . . . 6
β’ (β β π₯, π§ β β β¦ Xπ β
π₯ if(π = β, (-β(,)π§), β)) = (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) |
44 | 43 | a1i 11 |
. . . . 5
β’ (π€ = π₯ β (β β π₯, π§ β β β¦ Xπ β
π₯ if(π = β, (-β(,)π§), β)) = (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
45 | 36, 44 | eqtrd 2777 |
. . . 4
β’ (π€ = π₯ β (β β π€, π§ β β β¦ Xπ β
π€ if(π = β, (-β(,)π§), β)) = (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
46 | 45 | cbvmptv 5216 |
. . 3
β’ (π€ β Fin β¦ (β β π€, π§ β β β¦ Xπ β
π€ if(π = β, (-β(,)π§), β))) = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
47 | 21, 23, 17, 25, 27, 46 | hoimbllem 44772 |
. 2
β’ ((π β§ Β¬ π = β
) β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π) |
48 | 20, 47 | pm2.61dan 811 |
1
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π) |