Step | Hyp | Ref
| Expression |
1 | | xpsds.t |
. . 3
β’ π = (π
Γs π) |
2 | | xpsds.x |
. . 3
β’ π = (Baseβπ
) |
3 | | xpsds.y |
. . 3
β’ π = (Baseβπ) |
4 | | xpsds.1 |
. . 3
β’ (π β π
β π) |
5 | | xpsds.2 |
. . 3
β’ (π β π β π) |
6 | | eqid 2736 |
. . 3
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
7 | | eqid 2736 |
. . 3
β’
(Scalarβπ
) =
(Scalarβπ
) |
8 | | eqid 2736 |
. . 3
β’
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17326 |
. 2
β’ (π β π = (β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})
βs ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17327 |
. 2
β’ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
11 | 6 | xpsff1o2 17325 |
. . 3
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
12 | | f1ocnv 6758 |
. . 3
β’ ((π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):(π Γ π)β1-1-ontoβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ(π Γ π)) |
13 | 11, 12 | mp1i 13 |
. 2
β’ (π β β‘(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}):ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})β1-1-ontoβ(π Γ π)) |
14 | | ovexd 7342 |
. 2
β’ (π β ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) β
V) |
15 | | eqid 2736 |
. 2
β’
((distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) βΎ (ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) Γ ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) =
((distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) βΎ (ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) Γ ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) |
16 | | xpsds.p |
. 2
β’ π = (distβπ) |
17 | | eqid 2736 |
. . . . 5
β’
((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) = ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
18 | | eqid 2736 |
. . . . 5
β’
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) = (Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
19 | | eqid 2736 |
. . . . 5
β’
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)) |
20 | | eqid 2736 |
. . . . 5
β’
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) =
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) |
21 | | eqid 2736 |
. . . . 5
β’
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) = (distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
22 | | fvexd 6819 |
. . . . 5
β’ (π β (Scalarβπ
) β V) |
23 | | 2onn 8503 |
. . . . . 6
β’
2o β Ο |
24 | | nnfi 8988 |
. . . . . 6
β’
(2o β Ο β 2o β
Fin) |
25 | 23, 24 | mp1i 13 |
. . . . 5
β’ (π β 2o β
Fin) |
26 | | fvexd 6819 |
. . . . 5
β’ ((π β§ π β 2o) β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) β V) |
27 | | elpri 4587 |
. . . . . . 7
β’ (π β {β
, 1o}
β (π = β
β¨
π =
1o)) |
28 | | df2o3 8336 |
. . . . . . 7
β’
2o = {β
, 1o} |
29 | 27, 28 | eleq2s 2855 |
. . . . . 6
β’ (π β 2o β
(π = β
β¨ π =
1o)) |
30 | | xpsmet.3 |
. . . . . . . . 9
β’ (π β π β (Metβπ)) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π = β
) β π β (Metβπ)) |
32 | | fveq2 6804 |
. . . . . . . . . . . 12
β’ (π = β
β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = ({β¨β
, π
β©, β¨1o, πβ©}ββ
)) |
33 | | fvpr0o 17315 |
. . . . . . . . . . . . 13
β’ (π
β π β ({β¨β
, π
β©, β¨1o, πβ©}ββ
) = π
) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}ββ
) =
π
) |
35 | 32, 34 | sylan9eqr 2798 |
. . . . . . . . . . 11
β’ ((π β§ π = β
) β ({β¨β
, π
β©, β¨1o,
πβ©}βπ) = π
) |
36 | 35 | fveq2d 6808 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β
(distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (distβπ
)) |
37 | 35 | fveq2d 6808 |
. . . . . . . . . . . 12
β’ ((π β§ π = β
) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβπ
)) |
38 | 37, 2 | eqtr4di 2794 |
. . . . . . . . . . 11
β’ ((π β§ π = β
) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = π) |
39 | 38 | sqxpeqd 5632 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β
((Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ))) = (π Γ π)) |
40 | 36, 39 | reseq12d 5904 |
. . . . . . . . 9
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = ((distβπ
) βΎ (π Γ π))) |
41 | | xpsds.m |
. . . . . . . . 9
β’ π = ((distβπ
) βΎ (π Γ π)) |
42 | 40, 41 | eqtr4di 2794 |
. . . . . . . 8
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = π) |
43 | 38 | fveq2d 6808 |
. . . . . . . 8
β’ ((π β§ π = β
) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ))) = (Metβπ)) |
44 | 31, 42, 43 | 3eltr4d 2852 |
. . . . . . 7
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
45 | | xpsmet.4 |
. . . . . . . . 9
β’ (π β π β (Metβπ)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π = 1o) β π β (Metβπ)) |
47 | | fveq2 6804 |
. . . . . . . . . . . 12
β’ (π = 1o β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = ({β¨β
, π
β©, β¨1o, πβ©}β1o)) |
48 | | fvpr1o 17316 |
. . . . . . . . . . . . 13
β’ (π β π β ({β¨β
, π
β©, β¨1o, πβ©}β1o) =
π) |
49 | 5, 48 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}β1o) = π) |
50 | 47, 49 | sylan9eqr 2798 |
. . . . . . . . . . 11
β’ ((π β§ π = 1o) β ({β¨β
,
π
β©,
β¨1o, πβ©}βπ) = π) |
51 | 50 | fveq2d 6808 |
. . . . . . . . . 10
β’ ((π β§ π = 1o) β
(distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (distβπ)) |
52 | 50 | fveq2d 6808 |
. . . . . . . . . . . 12
β’ ((π β§ π = 1o) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβπ)) |
53 | 52, 3 | eqtr4di 2794 |
. . . . . . . . . . 11
β’ ((π β§ π = 1o) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = π) |
54 | 53 | sqxpeqd 5632 |
. . . . . . . . . 10
β’ ((π β§ π = 1o) β
((Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ))) = (π Γ π)) |
55 | 51, 54 | reseq12d 5904 |
. . . . . . . . 9
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = ((distβπ) βΎ (π Γ π))) |
56 | | xpsds.n |
. . . . . . . . 9
β’ π = ((distβπ) βΎ (π Γ π)) |
57 | 55, 56 | eqtr4di 2794 |
. . . . . . . 8
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = π) |
58 | 53 | fveq2d 6808 |
. . . . . . . 8
β’ ((π β§ π = 1o) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ))) = (Metβπ)) |
59 | 46, 57, 58 | 3eltr4d 2852 |
. . . . . . 7
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
60 | 44, 59 | jaodan 956 |
. . . . . 6
β’ ((π β§ (π = β
β¨ π = 1o)) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
61 | 29, 60 | sylan2 594 |
. . . . 5
β’ ((π β§ π β 2o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(Metβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
62 | 17, 18, 19, 20, 21, 22, 25, 26, 61 | prdsmet 23568 |
. . . 4
β’ (π β
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) β
(Metβ(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))))) |
63 | | fnpr2o 17313 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β {β¨β
, π
β©, β¨1o, πβ©} Fn
2o) |
64 | 4, 5, 63 | syl2anc 585 |
. . . . . . 7
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} Fn
2o) |
65 | | dffn5 6860 |
. . . . . . 7
β’
({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β
{β¨β
, π
β©,
β¨1o, πβ©} = (π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
66 | 64, 65 | sylib 217 |
. . . . . 6
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} = (π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
67 | 66 | oveq2d 7323 |
. . . . 5
β’ (π β ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
68 | 67 | fveq2d 6808 |
. . . 4
β’ (π β
(distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
69 | 67 | fveq2d 6808 |
. . . . . 6
β’ (π β
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
70 | 10, 69 | eqtrd 2776 |
. . . . 5
β’ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
71 | 70 | fveq2d 6808 |
. . . 4
β’ (π β (Metβran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) =
(Metβ(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))))) |
72 | 62, 68, 71 | 3eltr4d 2852 |
. . 3
β’ (π β
(distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β (Metβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) |
73 | | ssid 3948 |
. . 3
β’ ran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
74 | | metres2 23561 |
. . 3
β’
(((distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β (Metβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) β§ ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) β
((distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) βΎ (ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) Γ ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) β (Metβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) |
75 | 72, 73, 74 | sylancl 587 |
. 2
β’ (π β
((distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) βΎ (ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) Γ ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) β (Metβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) |
76 | 9, 10, 13, 14, 15, 16, 75 | imasf1omet 23574 |
1
β’ (π β π β (Metβ(π Γ π))) |