Step |
Hyp |
Ref |
Expression |
1 |
|
prdsdsf.y |
|- Y = ( S Xs_ ( x e. I |-> R ) ) |
2 |
|
prdsdsf.b |
|- B = ( Base ` Y ) |
3 |
|
prdsdsf.v |
|- V = ( Base ` R ) |
4 |
|
prdsdsf.e |
|- E = ( ( dist ` R ) |` ( V X. V ) ) |
5 |
|
prdsdsf.d |
|- D = ( dist ` Y ) |
6 |
|
prdsdsf.s |
|- ( ph -> S e. W ) |
7 |
|
prdsdsf.i |
|- ( ph -> I e. X ) |
8 |
|
prdsdsf.r |
|- ( ( ph /\ x e. I ) -> R e. Z ) |
9 |
|
prdsdsf.m |
|- ( ( ph /\ x e. I ) -> E e. ( *Met ` V ) ) |
10 |
|
nfcv |
|- F/_ y R |
11 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ R |
12 |
|
csbeq1a |
|- ( x = y -> R = [_ y / x ]_ R ) |
13 |
10 11 12
|
cbvmpt |
|- ( x e. I |-> R ) = ( y e. I |-> [_ y / x ]_ R ) |
14 |
13
|
oveq2i |
|- ( S Xs_ ( x e. I |-> R ) ) = ( S Xs_ ( y e. I |-> [_ y / x ]_ R ) ) |
15 |
1 14
|
eqtri |
|- Y = ( S Xs_ ( y e. I |-> [_ y / x ]_ R ) ) |
16 |
|
eqid |
|- ( Base ` [_ y / x ]_ R ) = ( Base ` [_ y / x ]_ R ) |
17 |
|
eqid |
|- ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) |
18 |
8
|
elexd |
|- ( ( ph /\ x e. I ) -> R e. _V ) |
19 |
18
|
ralrimiva |
|- ( ph -> A. x e. I R e. _V ) |
20 |
11
|
nfel1 |
|- F/ x [_ y / x ]_ R e. _V |
21 |
12
|
eleq1d |
|- ( x = y -> ( R e. _V <-> [_ y / x ]_ R e. _V ) ) |
22 |
20 21
|
rspc |
|- ( y e. I -> ( A. x e. I R e. _V -> [_ y / x ]_ R e. _V ) ) |
23 |
19 22
|
mpan9 |
|- ( ( ph /\ y e. I ) -> [_ y / x ]_ R e. _V ) |
24 |
9
|
ralrimiva |
|- ( ph -> A. x e. I E e. ( *Met ` V ) ) |
25 |
|
nfcv |
|- F/_ x dist |
26 |
25 11
|
nffv |
|- F/_ x ( dist ` [_ y / x ]_ R ) |
27 |
|
nfcv |
|- F/_ x Base |
28 |
27 11
|
nffv |
|- F/_ x ( Base ` [_ y / x ]_ R ) |
29 |
28 28
|
nfxp |
|- F/_ x ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) |
30 |
26 29
|
nfres |
|- F/_ x ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) |
31 |
|
nfcv |
|- F/_ x *Met |
32 |
31 28
|
nffv |
|- F/_ x ( *Met ` ( Base ` [_ y / x ]_ R ) ) |
33 |
30 32
|
nfel |
|- F/ x ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) |
34 |
12
|
fveq2d |
|- ( x = y -> ( dist ` R ) = ( dist ` [_ y / x ]_ R ) ) |
35 |
12
|
fveq2d |
|- ( x = y -> ( Base ` R ) = ( Base ` [_ y / x ]_ R ) ) |
36 |
3 35
|
syl5eq |
|- ( x = y -> V = ( Base ` [_ y / x ]_ R ) ) |
37 |
36
|
sqxpeqd |
|- ( x = y -> ( V X. V ) = ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) |
38 |
34 37
|
reseq12d |
|- ( x = y -> ( ( dist ` R ) |` ( V X. V ) ) = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) ) |
39 |
4 38
|
syl5eq |
|- ( x = y -> E = ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) ) |
40 |
36
|
fveq2d |
|- ( x = y -> ( *Met ` V ) = ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) |
41 |
39 40
|
eleq12d |
|- ( x = y -> ( E e. ( *Met ` V ) <-> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) ) |
42 |
33 41
|
rspc |
|- ( y e. I -> ( A. x e. I E e. ( *Met ` V ) -> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) ) |
43 |
24 42
|
mpan9 |
|- ( ( ph /\ y e. I ) -> ( ( dist ` [_ y / x ]_ R ) |` ( ( Base ` [_ y / x ]_ R ) X. ( Base ` [_ y / x ]_ R ) ) ) e. ( *Met ` ( Base ` [_ y / x ]_ R ) ) ) |
44 |
15 2 16 17 5 6 7 23 43
|
prdsxmetlem |
|- ( ph -> D e. ( *Met ` B ) ) |