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