Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) = ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
2 | | eqid 2733 |
. . 3
β’
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) = (Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
3 | | eqid 2733 |
. . 3
β’
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)) |
4 | | eqid 2733 |
. . 3
β’
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) =
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) |
5 | | eqid 2733 |
. . 3
β’
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) = (distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
6 | | fvexd 6907 |
. . 3
β’ (π β (Scalarβπ
) β V) |
7 | | 2on 8480 |
. . . 4
β’
2o β On |
8 | 7 | a1i 11 |
. . 3
β’ (π β 2o β
On) |
9 | | fvexd 6907 |
. . 3
β’ ((π β§ π β 2o) β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) β V) |
10 | | elpri 4651 |
. . . . 5
β’ (π β {β
, 1o}
β (π = β
β¨
π =
1o)) |
11 | | df2o3 8474 |
. . . . 5
β’
2o = {β
, 1o} |
12 | 10, 11 | eleq2s 2852 |
. . . 4
β’ (π β 2o β
(π = β
β¨ π =
1o)) |
13 | | xpsds.3 |
. . . . . . 7
β’ (π β π β (βMetβπ)) |
14 | 13 | adantr 482 |
. . . . . 6
β’ ((π β§ π = β
) β π β (βMetβπ)) |
15 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = β
β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = ({β¨β
, π
β©, β¨1o, πβ©}ββ
)) |
16 | | xpsds.1 |
. . . . . . . . . . 11
β’ (π β π
β π) |
17 | | fvpr0o 17505 |
. . . . . . . . . . 11
β’ (π
β π β ({β¨β
, π
β©, β¨1o, πβ©}ββ
) = π
) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}ββ
) =
π
) |
19 | 15, 18 | sylan9eqr 2795 |
. . . . . . . . 9
β’ ((π β§ π = β
) β ({β¨β
, π
β©, β¨1o,
πβ©}βπ) = π
) |
20 | 19 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π = β
) β
(distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (distβπ
)) |
21 | 19 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π β§ π = β
) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβπ
)) |
22 | | xpsds.x |
. . . . . . . . . 10
β’ π = (Baseβπ
) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π β§ π = β
) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = π) |
24 | 23 | sqxpeqd 5709 |
. . . . . . . 8
β’ ((π β§ π = β
) β
((Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ))) = (π Γ π)) |
25 | 20, 24 | reseq12d 5983 |
. . . . . . 7
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = ((distβπ
) βΎ (π Γ π))) |
26 | | xpsds.m |
. . . . . . 7
β’ π = ((distβπ
) βΎ (π Γ π)) |
27 | 25, 26 | eqtr4di 2791 |
. . . . . 6
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = π) |
28 | 23 | fveq2d 6896 |
. . . . . 6
β’ ((π β§ π = β
) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ))) = (βMetβπ)) |
29 | 14, 27, 28 | 3eltr4d 2849 |
. . . . 5
β’ ((π β§ π = β
) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
30 | | xpsds.4 |
. . . . . . 7
β’ (π β π β (βMetβπ)) |
31 | 30 | adantr 482 |
. . . . . 6
β’ ((π β§ π = 1o) β π β (βMetβπ)) |
32 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = 1o β
({β¨β
, π
β©,
β¨1o, πβ©}βπ) = ({β¨β
, π
β©, β¨1o, πβ©}β1o)) |
33 | | xpsds.2 |
. . . . . . . . . . 11
β’ (π β π β π) |
34 | | fvpr1o 17506 |
. . . . . . . . . . 11
β’ (π β π β ({β¨β
, π
β©, β¨1o, πβ©}β1o) =
π) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
β’ (π β ({β¨β
, π
β©, β¨1o,
πβ©}β1o) = π) |
36 | 32, 35 | sylan9eqr 2795 |
. . . . . . . . 9
β’ ((π β§ π = 1o) β ({β¨β
,
π
β©,
β¨1o, πβ©}βπ) = π) |
37 | 36 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π = 1o) β
(distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (distβπ)) |
38 | 36 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π β§ π = 1o) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = (Baseβπ)) |
39 | | xpsds.y |
. . . . . . . . . 10
β’ π = (Baseβπ) |
40 | 38, 39 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π β§ π = 1o) β
(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) = π) |
41 | 40 | sqxpeqd 5709 |
. . . . . . . 8
β’ ((π β§ π = 1o) β
((Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ))) = (π Γ π)) |
42 | 37, 41 | reseq12d 5983 |
. . . . . . 7
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = ((distβπ) βΎ (π Γ π))) |
43 | | xpsds.n |
. . . . . . 7
β’ π = ((distβπ) βΎ (π Γ π)) |
44 | 42, 43 | eqtr4di 2791 |
. . . . . 6
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) = π) |
45 | 40 | fveq2d 6896 |
. . . . . 6
β’ ((π β§ π = 1o) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ))) = (βMetβπ)) |
46 | 31, 44, 45 | 3eltr4d 2849 |
. . . . 5
β’ ((π β§ π = 1o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
47 | 29, 46 | jaodan 957 |
. . . 4
β’ ((π β§ (π = β
β¨ π = 1o)) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
48 | 12, 47 | sylan2 594 |
. . 3
β’ ((π β§ π β 2o) β
((distβ({β¨β
, π
β©, β¨1o, πβ©}βπ)) βΎ ((Baseβ({β¨β
,
π
β©,
β¨1o, πβ©}βπ)) Γ (Baseβ({β¨β
, π
β©, β¨1o,
πβ©}βπ)))) β
(βMetβ(Baseβ({β¨β
, π
β©, β¨1o, πβ©}βπ)))) |
49 | 1, 2, 3, 4, 5, 6, 8, 9, 48 | prdsxmet 23875 |
. 2
β’ (π β
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) β
(βMetβ(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))))) |
50 | | fnpr2o 17503 |
. . . . . 6
β’ ((π
β π β§ π β π) β {β¨β
, π
β©, β¨1o, πβ©} Fn
2o) |
51 | 16, 33, 50 | syl2anc 585 |
. . . . 5
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} Fn
2o) |
52 | | dffn5 6951 |
. . . . 5
β’
({β¨β
, π
β©, β¨1o, πβ©} Fn 2o β
{β¨β
, π
β©,
β¨1o, πβ©} = (π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
53 | 51, 52 | sylib 217 |
. . . 4
β’ (π β {β¨β
, π
β©, β¨1o,
πβ©} = (π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))) |
54 | 53 | oveq2d 7425 |
. . 3
β’ (π β ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))) |
55 | 54 | fveq2d 6896 |
. 2
β’ (π β
(distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(distβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
56 | | xpsds.t |
. . . . 5
β’ π = (π
Γs π) |
57 | | eqid 2733 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
58 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ
) =
(Scalarβπ
) |
59 | | eqid 2733 |
. . . . 5
β’
((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) = ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}) |
60 | 56, 22, 39, 16, 33, 57, 58, 59 | xpsrnbas 17517 |
. . . 4
β’ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©}))) |
61 | 54 | fveq2d 6896 |
. . . 4
β’ (π β
(Baseβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) =
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
62 | 60, 61 | eqtrd 2773 |
. . 3
β’ (π β ran (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) =
(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ))))) |
63 | 62 | fveq2d 6896 |
. 2
β’ (π β (βMetβran
(π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) =
(βMetβ(Baseβ((Scalarβπ
)Xs(π β 2o β¦
({β¨β
, π
β©,
β¨1o, πβ©}βπ)))))) |
64 | 49, 55, 63 | 3eltr4d 2849 |
1
β’ (π β
(distβ((Scalarβπ
)Xs{β¨β
, π
β©, β¨1o, πβ©})) β
(βMetβran (π₯
β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}))) |