Step | Hyp | Ref
| Expression |
1 | | prdsdsf.y |
. . 3
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | nfcv 2904 |
. . . . 5
β’
β²π¦π
|
3 | | nfcsb1v 3881 |
. . . . 5
β’
β²π₯β¦π¦ / π₯β¦π
|
4 | | csbeq1a 3870 |
. . . . 5
β’ (π₯ = π¦ β π
= β¦π¦ / π₯β¦π
) |
5 | 2, 3, 4 | cbvmpt 5217 |
. . . 4
β’ (π₯ β πΌ β¦ π
) = (π¦ β πΌ β¦ β¦π¦ / π₯β¦π
) |
6 | 5 | oveq2i 7369 |
. . 3
β’ (πXs(π₯ β πΌ β¦ π
)) = (πXs(π¦ β πΌ β¦ β¦π¦ / π₯β¦π
)) |
7 | 1, 6 | eqtri 2761 |
. 2
β’ π = (πXs(π¦ β πΌ β¦ β¦π¦ / π₯β¦π
)) |
8 | | prdsdsf.b |
. 2
β’ π΅ = (Baseβπ) |
9 | | eqid 2733 |
. 2
β’
(Baseββ¦π¦ / π₯β¦π
) = (Baseββ¦π¦ / π₯β¦π
) |
10 | | eqid 2733 |
. 2
β’
((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) = ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) |
11 | | prdsdsf.d |
. 2
β’ π· = (distβπ) |
12 | | prdsdsf.s |
. 2
β’ (π β π β π) |
13 | | prdsdsf.i |
. 2
β’ (π β πΌ β π) |
14 | | prdsdsf.r |
. . . . 5
β’ ((π β§ π₯ β πΌ) β π
β π) |
15 | 14 | elexd 3464 |
. . . 4
β’ ((π β§ π₯ β πΌ) β π
β V) |
16 | 15 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β πΌ π
β V) |
17 | 3 | nfel1 2920 |
. . . 4
β’
β²π₯β¦π¦ / π₯β¦π
β V |
18 | 4 | eleq1d 2819 |
. . . 4
β’ (π₯ = π¦ β (π
β V β β¦π¦ / π₯β¦π
β V)) |
19 | 17, 18 | rspc 3568 |
. . 3
β’ (π¦ β πΌ β (βπ₯ β πΌ π
β V β β¦π¦ / π₯β¦π
β V)) |
20 | 16, 19 | mpan9 508 |
. 2
β’ ((π β§ π¦ β πΌ) β β¦π¦ / π₯β¦π
β V) |
21 | | prdsdsf.m |
. . . 4
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
22 | 21 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β πΌ πΈ β (βMetβπ)) |
23 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯dist |
24 | 23, 3 | nffv 6853 |
. . . . . 6
β’
β²π₯(distββ¦π¦ / π₯β¦π
) |
25 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯Base |
26 | 25, 3 | nffv 6853 |
. . . . . . 7
β’
β²π₯(Baseββ¦π¦ / π₯β¦π
) |
27 | 26, 26 | nfxp 5667 |
. . . . . 6
β’
β²π₯((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)) |
28 | 24, 27 | nfres 5940 |
. . . . 5
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) |
29 | | nfcv 2904 |
. . . . . 6
β’
β²π₯βMet |
30 | 29, 26 | nffv 6853 |
. . . . 5
β’
β²π₯(βMetβ(Baseββ¦π¦ / π₯β¦π
)) |
31 | 28, 30 | nfel 2918 |
. . . 4
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)) |
32 | | prdsdsf.e |
. . . . . 6
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
33 | 4 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π¦ β (distβπ
) = (distββ¦π¦ / π₯β¦π
)) |
34 | | prdsdsf.v |
. . . . . . . . 9
β’ π = (Baseβπ
) |
35 | 4 | fveq2d 6847 |
. . . . . . . . 9
β’ (π₯ = π¦ β (Baseβπ
) = (Baseββ¦π¦ / π₯β¦π
)) |
36 | 34, 35 | eqtrid 2785 |
. . . . . . . 8
β’ (π₯ = π¦ β π = (Baseββ¦π¦ / π₯β¦π
)) |
37 | 36 | sqxpeqd 5666 |
. . . . . . 7
β’ (π₯ = π¦ β (π Γ π) = ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) |
38 | 33, 37 | reseq12d 5939 |
. . . . . 6
β’ (π₯ = π¦ β ((distβπ
) βΎ (π Γ π)) = ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)))) |
39 | 32, 38 | eqtrid 2785 |
. . . . 5
β’ (π₯ = π¦ β πΈ = ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)))) |
40 | 36 | fveq2d 6847 |
. . . . 5
β’ (π₯ = π¦ β (βMetβπ) =
(βMetβ(Baseββ¦π¦ / π₯β¦π
))) |
41 | 39, 40 | eleq12d 2828 |
. . . 4
β’ (π₯ = π¦ β (πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)))) |
42 | 31, 41 | rspc 3568 |
. . 3
β’ (π¦ β πΌ β (βπ₯ β πΌ πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)))) |
43 | 22, 42 | mpan9 508 |
. 2
β’ ((π β§ π¦ β πΌ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
))) |
44 | 7, 8, 9, 10, 11, 12, 13, 20, 43 | prdsxmetlem 23737 |
1
β’ (π β π· β (βMetβπ΅)) |