Step | Hyp | Ref
| Expression |
1 | | prdsdsf.y |
. . 3
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | nfcv 2903 |
. . . . 5
β’
β²π¦π
|
3 | | nfcsb1v 3918 |
. . . . 5
β’
β²π₯β¦π¦ / π₯β¦π
|
4 | | csbeq1a 3907 |
. . . . 5
β’ (π₯ = π¦ β π
= β¦π¦ / π₯β¦π
) |
5 | 2, 3, 4 | cbvmpt 5259 |
. . . 4
β’ (π₯ β πΌ β¦ π
) = (π¦ β πΌ β¦ β¦π¦ / π₯β¦π
) |
6 | 5 | oveq2i 7419 |
. . 3
β’ (πXs(π₯ β πΌ β¦ π
)) = (πXs(π¦ β πΌ β¦ β¦π¦ / π₯β¦π
)) |
7 | 1, 6 | eqtri 2760 |
. 2
β’ π = (πXs(π¦ β πΌ β¦ β¦π¦ / π₯β¦π
)) |
8 | | prdsdsf.b |
. 2
β’ π΅ = (Baseβπ) |
9 | | eqid 2732 |
. 2
β’
(Baseββ¦π¦ / π₯β¦π
) = (Baseββ¦π¦ / π₯β¦π
) |
10 | | eqid 2732 |
. 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 3494 |
. . . 4
β’ ((π β§ π₯ β πΌ) β π
β V) |
16 | 15 | ralrimiva 3146 |
. . 3
β’ (π β βπ₯ β πΌ π
β V) |
17 | 3 | nfel1 2919 |
. . . 4
β’
β²π₯β¦π¦ / π₯β¦π
β V |
18 | 4 | eleq1d 2818 |
. . . 4
β’ (π₯ = π¦ β (π
β V β β¦π¦ / π₯β¦π
β V)) |
19 | 17, 18 | rspc 3600 |
. . 3
β’ (π¦ β πΌ β (βπ₯ β πΌ π
β V β β¦π¦ / π₯β¦π
β V)) |
20 | 16, 19 | mpan9 507 |
. 2
β’ ((π β§ π¦ β πΌ) β β¦π¦ / π₯β¦π
β V) |
21 | | prdsdsf.m |
. . . 4
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
22 | 21 | ralrimiva 3146 |
. . 3
β’ (π β βπ₯ β πΌ πΈ β (βMetβπ)) |
23 | | nfcv 2903 |
. . . . . . 7
β’
β²π₯dist |
24 | 23, 3 | nffv 6901 |
. . . . . 6
β’
β²π₯(distββ¦π¦ / π₯β¦π
) |
25 | | nfcv 2903 |
. . . . . . . 8
β’
β²π₯Base |
26 | 25, 3 | nffv 6901 |
. . . . . . 7
β’
β²π₯(Baseββ¦π¦ / π₯β¦π
) |
27 | 26, 26 | nfxp 5709 |
. . . . . 6
β’
β²π₯((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)) |
28 | 24, 27 | nfres 5983 |
. . . . 5
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) |
29 | | nfcv 2903 |
. . . . . 6
β’
β²π₯βMet |
30 | 29, 26 | nffv 6901 |
. . . . 5
β’
β²π₯(βMetβ(Baseββ¦π¦ / π₯β¦π
)) |
31 | 28, 30 | nfel 2917 |
. . . 4
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)) |
32 | | prdsdsf.e |
. . . . . 6
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
33 | 4 | fveq2d 6895 |
. . . . . . 7
β’ (π₯ = π¦ β (distβπ
) = (distββ¦π¦ / π₯β¦π
)) |
34 | | prdsdsf.v |
. . . . . . . . 9
β’ π = (Baseβπ
) |
35 | 4 | fveq2d 6895 |
. . . . . . . . 9
β’ (π₯ = π¦ β (Baseβπ
) = (Baseββ¦π¦ / π₯β¦π
)) |
36 | 34, 35 | eqtrid 2784 |
. . . . . . . 8
β’ (π₯ = π¦ β π = (Baseββ¦π¦ / π₯β¦π
)) |
37 | 36 | sqxpeqd 5708 |
. . . . . . 7
β’ (π₯ = π¦ β (π Γ π) = ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) |
38 | 33, 37 | reseq12d 5982 |
. . . . . 6
β’ (π₯ = π¦ β ((distβπ
) βΎ (π Γ π)) = ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)))) |
39 | 32, 38 | eqtrid 2784 |
. . . . 5
β’ (π₯ = π¦ β πΈ = ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
)))) |
40 | 36 | fveq2d 6895 |
. . . . 5
β’ (π₯ = π¦ β (βMetβπ) =
(βMetβ(Baseββ¦π¦ / π₯β¦π
))) |
41 | 39, 40 | eleq12d 2827 |
. . . 4
β’ (π₯ = π¦ β (πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)))) |
42 | 31, 41 | rspc 3600 |
. . 3
β’ (π¦ β πΌ β (βπ₯ β πΌ πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
)))) |
43 | 22, 42 | mpan9 507 |
. 2
β’ ((π β§ π¦ β πΌ) β ((distββ¦π¦ / π₯β¦π
) βΎ ((Baseββ¦π¦ / π₯β¦π
) Γ (Baseββ¦π¦ / π₯β¦π
))) β
(βMetβ(Baseββ¦π¦ / π₯β¦π
))) |
44 | 7, 8, 9, 10, 11, 12, 13, 20, 43 | prdsxmetlem 23873 |
1
β’ (π β π· β (βMetβπ΅)) |