Step | Hyp | Ref
| Expression |
1 | | fvexd 6858 |
. . 3
β’ (π€ = π β (Baseβπ€) β V) |
2 | | fveq2 6843 |
. . . . . . 7
β’ (π€ = π β (distβπ€) = (distβπ)) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((π€ = π β§ π = (Baseβπ€)) β (distβπ€) = (distβπ)) |
4 | | id 22 |
. . . . . . . 8
β’ (π = (Baseβπ€) β π = (Baseβπ€)) |
5 | | fveq2 6843 |
. . . . . . . . 9
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
6 | | iscms.1 |
. . . . . . . . 9
β’ π = (Baseβπ) |
7 | 5, 6 | eqtr4di 2795 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = π) |
8 | 4, 7 | sylan9eqr 2799 |
. . . . . . 7
β’ ((π€ = π β§ π = (Baseβπ€)) β π = π) |
9 | 8 | sqxpeqd 5666 |
. . . . . 6
β’ ((π€ = π β§ π = (Baseβπ€)) β (π Γ π) = (π Γ π)) |
10 | 3, 9 | reseq12d 5939 |
. . . . 5
β’ ((π€ = π β§ π = (Baseβπ€)) β ((distβπ€) βΎ (π Γ π)) = ((distβπ) βΎ (π Γ π))) |
11 | | iscms.2 |
. . . . 5
β’ π· = ((distβπ) βΎ (π Γ π)) |
12 | 10, 11 | eqtr4di 2795 |
. . . 4
β’ ((π€ = π β§ π = (Baseβπ€)) β ((distβπ€) βΎ (π Γ π)) = π·) |
13 | 8 | fveq2d 6847 |
. . . 4
β’ ((π€ = π β§ π = (Baseβπ€)) β (CMetβπ) = (CMetβπ)) |
14 | 12, 13 | eleq12d 2832 |
. . 3
β’ ((π€ = π β§ π = (Baseβπ€)) β (((distβπ€) βΎ (π Γ π)) β (CMetβπ) β π· β (CMetβπ))) |
15 | 1, 14 | sbcied 3785 |
. 2
β’ (π€ = π β ([(Baseβπ€) / π]((distβπ€) βΎ (π Γ π)) β (CMetβπ) β π· β (CMetβπ))) |
16 | | df-cms 24702 |
. 2
β’ CMetSp =
{π€ β MetSp β£
[(Baseβπ€) /
π]((distβπ€) βΎ (π Γ π)) β (CMetβπ)} |
17 | 15, 16 | elrab2 3649 |
1
β’ (π β CMetSp β (π β MetSp β§ π· β (CMetβπ))) |