Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . 3
β’ (π β π = (πΉ βs π
)) |
2 | | imasbas.v |
. . 3
β’ (π β π = (Baseβπ
)) |
3 | | imasbas.f |
. . 3
β’ (π β πΉ:πβontoβπ΅) |
4 | | imasbas.r |
. . 3
β’ (π β π
β π) |
5 | | imasds.e |
. . 3
β’ πΈ = (distβπ
) |
6 | | imasds.d |
. . 3
β’ π· = (distβπ) |
7 | 1, 2, 3, 4, 5, 6 | imasds 17396 |
. 2
β’ (π β π· = (π₯ β π΅, π¦ β π΅ β¦ inf(βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g (πΈ β π))), β*, <
))) |
8 | | simplrl 776 |
. . . . . . . . . 10
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β π₯ = π) |
9 | 8 | eqeq2d 2748 |
. . . . . . . . 9
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β ((πΉβ(1st β(ββ1))) = π₯ β (πΉβ(1st β(ββ1))) = π)) |
10 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β π¦ = π) |
11 | 10 | eqeq2d 2748 |
. . . . . . . . 9
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β ((πΉβ(2nd β(ββπ))) = π¦ β (πΉβ(2nd β(ββπ))) = π)) |
12 | 9, 11 | 3anbi12d 1438 |
. . . . . . . 8
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β (((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1))))) β ((πΉβ(1st β(ββ1))) = π β§ (πΉβ(2nd β(ββπ))) = π β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1))))))) |
13 | 12 | rabbidv 3416 |
. . . . . . 7
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} = {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π β§ (πΉβ(2nd β(ββπ))) = π β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))}) |
14 | | imasdsval.s |
. . . . . . 7
β’ π = {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π β§ (πΉβ(2nd β(ββπ))) = π β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} |
15 | 13, 14 | eqtr4di 2795 |
. . . . . 6
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} = π) |
16 | 15 | mpteq1d 5201 |
. . . . 5
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g (πΈ β π))) = (π β π β¦
(β*π Ξ£g (πΈ β π)))) |
17 | 16 | rneqd 5894 |
. . . 4
β’ (((π β§ (π₯ = π β§ π¦ = π)) β§ π β β) β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g (πΈ β π))) = ran (π β π β¦
(β*π Ξ£g (πΈ β π)))) |
18 | 17 | iuneq2dv 4979 |
. . 3
β’ ((π β§ (π₯ = π β§ π¦ = π)) β βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g (πΈ β π))) = βͺ
π β β ran (π β π β¦
(β*π Ξ£g (πΈ β π)))) |
19 | 18 | infeq1d 9414 |
. 2
β’ ((π β§ (π₯ = π β§ π¦ = π)) β inf(βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g (πΈ β π))), β*, < ) =
inf(βͺ π β β ran (π β π β¦
(β*π Ξ£g (πΈ β π))), β*, <
)) |
20 | | imasdsval.x |
. 2
β’ (π β π β π΅) |
21 | | imasdsval.y |
. 2
β’ (π β π β π΅) |
22 | | xrltso 13061 |
. . . 4
β’ < Or
β* |
23 | 22 | infex 9430 |
. . 3
β’
inf(βͺ π β β ran (π β π β¦
(β*π Ξ£g (πΈ β π))), β*, < ) β
V |
24 | 23 | a1i 11 |
. 2
β’ (π β inf(βͺ π β β ran (π β π β¦
(β*π Ξ£g (πΈ β π))), β*, < ) β
V) |
25 | 7, 19, 20, 21, 24 | ovmpod 7508 |
1
β’ (π β (ππ·π) = inf(βͺ
π β β ran (π β π β¦
(β*π Ξ£g (πΈ β π))), β*, <
)) |