Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . . 5
β’
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
2 | | fvexd 6900 |
. . . . 5
β’ ((π
β TopSp β§ π β TopSp) β
(Scalarβπ
) β
V) |
3 | | 2on 8481 |
. . . . . 6
β’
2o β On |
4 | 3 | a1i 11 |
. . . . 5
β’ ((π
β TopSp β§ π β TopSp) β
2o β On) |
5 | | fnpr2o 17512 |
. . . . 5
β’ ((π
β TopSp β§ π β TopSp) β
{β¨β
, π
β©,
β¨1o, πβ©} Fn 2o) |
6 | | eqid 2726 |
. . . . 5
β’
(TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) |
7 | 1, 2, 4, 5, 6 | prdstopn 23487 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(βtβ(TopOpen β {β¨β
, π
β©, β¨1o, πβ©}))) |
8 | | topnfn 17380 |
. . . . . . . 8
β’ TopOpen
Fn V |
9 | | dffn2 6713 |
. . . . . . . . 9
β’
({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β
{β¨β
, π
β©,
β¨1o, πβ©}:2oβΆV) |
10 | 5, 9 | sylib 217 |
. . . . . . . 8
β’ ((π
β TopSp β§ π β TopSp) β
{β¨β
, π
β©,
β¨1o, πβ©}:2oβΆV) |
11 | | fnfco 6750 |
. . . . . . . 8
β’ ((TopOpen
Fn V β§ {β¨β
, π
β©, β¨1o, πβ©}:2oβΆV)
β (TopOpen β {β¨β
, π
β©, β¨1o, πβ©}) Fn
2o) |
12 | 8, 10, 11 | sylancr 586 |
. . . . . . 7
β’ ((π
β TopSp β§ π β TopSp) β (TopOpen
β {β¨β
, π
β©, β¨1o, πβ©}) Fn
2o) |
13 | | xpsfeq 17518 |
. . . . . . 7
β’ ((TopOpen
β {β¨β
, π
β©, β¨1o, πβ©}) Fn 2o β
{β¨β
, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})ββ
)β©,
β¨1o, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})β1o)β©} =
(TopOpen β {β¨β
, π
β©, β¨1o, πβ©})) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ ((π
β TopSp β§ π β TopSp) β
{β¨β
, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})ββ
)β©,
β¨1o, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})β1o)β©} =
(TopOpen β {β¨β
, π
β©, β¨1o, πβ©})) |
15 | | 0ex 5300 |
. . . . . . . . . . . 12
β’ β
β V |
16 | 15 | prid1 4761 |
. . . . . . . . . . 11
β’ β
β {β
, 1o} |
17 | | df2o3 8475 |
. . . . . . . . . . 11
β’
2o = {β
, 1o} |
18 | 16, 17 | eleqtrri 2826 |
. . . . . . . . . 10
β’ β
β 2o |
19 | | fvco2 6982 |
. . . . . . . . . 10
β’
(({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β§
β
β 2o) β ((TopOpen β {β¨β
, π
β©, β¨1o,
πβ©})ββ
) =
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}ββ
))) |
20 | 5, 18, 19 | sylancl 585 |
. . . . . . . . 9
β’ ((π
β TopSp β§ π β TopSp) β ((TopOpen
β {β¨β
, π
β©, β¨1o, πβ©})ββ
) =
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}ββ
))) |
21 | | fvpr0o 17514 |
. . . . . . . . . . . 12
β’ (π
β TopSp β
({β¨β
, π
β©,
β¨1o, πβ©}ββ
) = π
) |
22 | 21 | adantr 480 |
. . . . . . . . . . 11
β’ ((π
β TopSp β§ π β TopSp) β
({β¨β
, π
β©,
β¨1o, πβ©}ββ
) = π
) |
23 | 22 | fveq2d 6889 |
. . . . . . . . . 10
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}ββ
)) =
(TopOpenβπ
)) |
24 | | xpstopn.j |
. . . . . . . . . 10
β’ π½ = (TopOpenβπ
) |
25 | 23, 24 | eqtr4di 2784 |
. . . . . . . . 9
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}ββ
)) = π½) |
26 | 20, 25 | eqtrd 2766 |
. . . . . . . 8
β’ ((π
β TopSp β§ π β TopSp) β ((TopOpen
β {β¨β
, π
β©, β¨1o, πβ©})ββ
) = π½) |
27 | 26 | opeq2d 4875 |
. . . . . . 7
β’ ((π
β TopSp β§ π β TopSp) β
β¨β
, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})ββ
)β© =
β¨β
, π½β©) |
28 | | 1oex 8477 |
. . . . . . . . . . . 12
β’
1o β V |
29 | 28 | prid2 4762 |
. . . . . . . . . . 11
β’
1o β {β
, 1o} |
30 | 29, 17 | eleqtrri 2826 |
. . . . . . . . . 10
β’
1o β 2o |
31 | | fvco2 6982 |
. . . . . . . . . 10
β’
(({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β§
1o β 2o) β ((TopOpen β {β¨β
,
π
β©,
β¨1o, πβ©})β1o) =
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}β1o))) |
32 | 5, 30, 31 | sylancl 585 |
. . . . . . . . 9
β’ ((π
β TopSp β§ π β TopSp) β ((TopOpen
β {β¨β
, π
β©, β¨1o, πβ©})β1o) =
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}β1o))) |
33 | | fvpr1o 17515 |
. . . . . . . . . . . 12
β’ (π β TopSp β
({β¨β
, π
β©,
β¨1o, πβ©}β1o) = π) |
34 | 33 | adantl 481 |
. . . . . . . . . . 11
β’ ((π
β TopSp β§ π β TopSp) β
({β¨β
, π
β©,
β¨1o, πβ©}β1o) = π) |
35 | 34 | fveq2d 6889 |
. . . . . . . . . 10
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}β1o)) =
(TopOpenβπ)) |
36 | | xpstopn.k |
. . . . . . . . . 10
β’ πΎ = (TopOpenβπ) |
37 | 35, 36 | eqtr4di 2784 |
. . . . . . . . 9
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ({β¨β
, π
β©, β¨1o, πβ©}β1o)) =
πΎ) |
38 | 32, 37 | eqtrd 2766 |
. . . . . . . 8
β’ ((π
β TopSp β§ π β TopSp) β ((TopOpen
β {β¨β
, π
β©, β¨1o, πβ©})β1o) =
πΎ) |
39 | 38 | opeq2d 4875 |
. . . . . . 7
β’ ((π
β TopSp β§ π β TopSp) β
β¨1o, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})β1o)β© =
β¨1o, πΎβ©) |
40 | 27, 39 | preq12d 4740 |
. . . . . 6
β’ ((π
β TopSp β§ π β TopSp) β
{β¨β
, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})ββ
)β©,
β¨1o, ((TopOpen β {β¨β
, π
β©, β¨1o, πβ©})β1o)β©} =
{β¨β
, π½β©,
β¨1o, πΎβ©}) |
41 | 14, 40 | eqtr3d 2768 |
. . . . 5
β’ ((π
β TopSp β§ π β TopSp) β (TopOpen
β {β¨β
, π
β©, β¨1o, πβ©}) = {β¨β
, π½β©, β¨1o,
πΎβ©}) |
42 | 41 | fveq2d 6889 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β
(βtβ(TopOpen β {β¨β
, π
β©, β¨1o, πβ©})) =
(βtβ{β¨β
, π½β©, β¨1o, πΎβ©})) |
43 | 7, 42 | eqtrd 2766 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β
(TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(βtβ{β¨β
, π½β©, β¨1o, πΎβ©})) |
44 | 43 | oveq1d 7420 |
. 2
β’ ((π
β TopSp β§ π β TopSp) β
((TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) qTop β‘πΉ) =
((βtβ{β¨β
, π½β©, β¨1o, πΎβ©}) qTop β‘πΉ)) |
45 | | xpstps.t |
. . . 4
β’ π = (π
Γs π) |
46 | | xpstopnlem.x |
. . . 4
β’ π = (Baseβπ
) |
47 | | xpstopnlem.y |
. . . 4
β’ π = (Baseβπ) |
48 | | simpl 482 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β π
β TopSp) |
49 | | simpr 484 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β π β TopSp) |
50 | | xpstopnlem.f |
. . . 4
β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
51 | | eqid 2726 |
. . . 4
β’
(Scalarβπ
) =
(Scalarβπ
) |
52 | 45, 46, 47, 48, 49, 50, 51, 1 | xpsval 17525 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β π = (β‘πΉ βs
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o,
πβ©}))) |
53 | 45, 46, 47, 48, 49, 50, 51, 1 | xpsrnbas 17526 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β ran πΉ =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
54 | 50 | xpsff1o2 17524 |
. . . . 5
β’ πΉ:(π Γ π)β1-1-ontoβran
πΉ |
55 | | f1ocnv 6839 |
. . . . 5
β’ (πΉ:(π Γ π)β1-1-ontoβran
πΉ β β‘πΉ:ran πΉβ1-1-ontoβ(π Γ π)) |
56 | 54, 55 | mp1i 13 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β β‘πΉ:ran πΉβ1-1-ontoβ(π Γ π)) |
57 | | f1ofo 6834 |
. . . 4
β’ (β‘πΉ:ran πΉβ1-1-ontoβ(π Γ π) β β‘πΉ:ran πΉβontoβ(π Γ π)) |
58 | 56, 57 | syl 17 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β β‘πΉ:ran πΉβontoβ(π Γ π)) |
59 | | ovexd 7440 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o,
πβ©}) β
V) |
60 | | xpstopn.o |
. . 3
β’ π = (TopOpenβπ) |
61 | 52, 53, 58, 59, 6, 60 | imastopn 23579 |
. 2
β’ ((π
β TopSp β§ π β TopSp) β π =
((TopOpenβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) qTop β‘πΉ)) |
62 | 46, 24 | istps 22791 |
. . . . 5
β’ (π
β TopSp β π½ β (TopOnβπ)) |
63 | 48, 62 | sylib 217 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β π½ β (TopOnβπ)) |
64 | 47, 36 | istps 22791 |
. . . . 5
β’ (π β TopSp β πΎ β (TopOnβπ)) |
65 | 49, 64 | sylib 217 |
. . . 4
β’ ((π
β TopSp β§ π β TopSp) β πΎ β (TopOnβπ)) |
66 | 50, 63, 65 | xpstopnlem1 23668 |
. . 3
β’ ((π
β TopSp β§ π β TopSp) β πΉ β ((π½ Γt πΎ)Homeo(βtβ{β¨β
,
π½β©, β¨1o,
πΎβ©}))) |
67 | | hmeocnv 23621 |
. . 3
β’ (πΉ β ((π½ Γt πΎ)Homeo(βtβ{β¨β
,
π½β©, β¨1o,
πΎβ©})) β β‘πΉ β
((βtβ{β¨β
, π½β©, β¨1o, πΎβ©})Homeo(π½ Γt πΎ))) |
68 | | hmeoqtop 23634 |
. . 3
β’ (β‘πΉ β
((βtβ{β¨β
, π½β©, β¨1o, πΎβ©})Homeo(π½ Γt πΎ)) β (π½ Γt πΎ) =
((βtβ{β¨β
, π½β©, β¨1o, πΎβ©}) qTop β‘πΉ)) |
69 | 66, 67, 68 | 3syl 18 |
. 2
β’ ((π
β TopSp β§ π β TopSp) β (π½ Γt πΎ) =
((βtβ{β¨β
, π½β©, β¨1o, πΎβ©}) qTop β‘πΉ)) |
70 | 44, 61, 69 | 3eqtr4d 2776 |
1
β’ ((π
β TopSp β§ π β TopSp) β π = (π½ Γt πΎ)) |