Step |
Hyp |
Ref |
Expression |
1 |
|
xpsds.t |
|- T = ( R Xs. S ) |
2 |
|
xpsds.x |
|- X = ( Base ` R ) |
3 |
|
xpsds.y |
|- Y = ( Base ` S ) |
4 |
|
xpsds.1 |
|- ( ph -> R e. V ) |
5 |
|
xpsds.2 |
|- ( ph -> S e. W ) |
6 |
|
xpsds.p |
|- P = ( dist ` T ) |
7 |
|
xpsds.m |
|- M = ( ( dist ` R ) |` ( X X. X ) ) |
8 |
|
xpsds.n |
|- N = ( ( dist ` S ) |` ( Y X. Y ) ) |
9 |
|
xpsmet.3 |
|- ( ph -> M e. ( Met ` X ) ) |
10 |
|
xpsmet.4 |
|- ( ph -> N e. ( Met ` Y ) ) |
11 |
|
eqid |
|- ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
12 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
13 |
|
eqid |
|- ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) |
14 |
1 2 3 4 5 11 12 13
|
xpsval |
|- ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
15 |
1 2 3 4 5 11 12 13
|
xpsrnbas |
|- ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
16 |
11
|
xpsff1o2 |
|- ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
17 |
|
f1ocnv |
|- ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) ) |
18 |
16 17
|
mp1i |
|- ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) ) |
19 |
|
ovexd |
|- ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V ) |
20 |
|
eqid |
|- ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) = ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
21 |
|
eqid |
|- ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) |
22 |
|
eqid |
|- ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
23 |
|
eqid |
|- ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |
24 |
|
eqid |
|- ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
25 |
|
eqid |
|- ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
26 |
|
fvexd |
|- ( ph -> ( Scalar ` R ) e. _V ) |
27 |
|
2onn |
|- 2o e. _om |
28 |
|
nnfi |
|- ( 2o e. _om -> 2o e. Fin ) |
29 |
27 28
|
mp1i |
|- ( ph -> 2o e. Fin ) |
30 |
|
fvexd |
|- ( ( ph /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) e. _V ) |
31 |
|
elpri |
|- ( k e. { (/) , 1o } -> ( k = (/) \/ k = 1o ) ) |
32 |
|
df2o3 |
|- 2o = { (/) , 1o } |
33 |
31 32
|
eleq2s |
|- ( k e. 2o -> ( k = (/) \/ k = 1o ) ) |
34 |
9
|
adantr |
|- ( ( ph /\ k = (/) ) -> M e. ( Met ` X ) ) |
35 |
|
fveq2 |
|- ( k = (/) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) |
36 |
|
fvpr0o |
|- ( R e. V -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R ) |
37 |
4 36
|
syl |
|- ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R ) |
38 |
35 37
|
sylan9eqr |
|- ( ( ph /\ k = (/) ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = R ) |
39 |
38
|
fveq2d |
|- ( ( ph /\ k = (/) ) -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` R ) ) |
40 |
38
|
fveq2d |
|- ( ( ph /\ k = (/) ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` R ) ) |
41 |
40 2
|
eqtr4di |
|- ( ( ph /\ k = (/) ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = X ) |
42 |
41
|
sqxpeqd |
|- ( ( ph /\ k = (/) ) -> ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( X X. X ) ) |
43 |
39 42
|
reseq12d |
|- ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` R ) |` ( X X. X ) ) ) |
44 |
43 7
|
eqtr4di |
|- ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = M ) |
45 |
41
|
fveq2d |
|- ( ( ph /\ k = (/) ) -> ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Met ` X ) ) |
46 |
34 44 45
|
3eltr4d |
|- ( ( ph /\ k = (/) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
47 |
10
|
adantr |
|- ( ( ph /\ k = 1o ) -> N e. ( Met ` Y ) ) |
48 |
|
fveq2 |
|- ( k = 1o -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) |
49 |
|
fvpr1o |
|- ( S e. W -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S ) |
50 |
5 49
|
syl |
|- ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S ) |
51 |
48 50
|
sylan9eqr |
|- ( ( ph /\ k = 1o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = S ) |
52 |
51
|
fveq2d |
|- ( ( ph /\ k = 1o ) -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` S ) ) |
53 |
51
|
fveq2d |
|- ( ( ph /\ k = 1o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` S ) ) |
54 |
53 3
|
eqtr4di |
|- ( ( ph /\ k = 1o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = Y ) |
55 |
54
|
sqxpeqd |
|- ( ( ph /\ k = 1o ) -> ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Y X. Y ) ) |
56 |
52 55
|
reseq12d |
|- ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = ( ( dist ` S ) |` ( Y X. Y ) ) ) |
57 |
56 8
|
eqtr4di |
|- ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) = N ) |
58 |
54
|
fveq2d |
|- ( ( ph /\ k = 1o ) -> ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) = ( Met ` Y ) ) |
59 |
47 57 58
|
3eltr4d |
|- ( ( ph /\ k = 1o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
60 |
46 59
|
jaodan |
|- ( ( ph /\ ( k = (/) \/ k = 1o ) ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
61 |
33 60
|
sylan2 |
|- ( ( ph /\ k e. 2o ) -> ( ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) |` ( ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) X. ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
62 |
21 22 23 24 25 26 29 30 61
|
prdsmet |
|- ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) e. ( Met ` ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) ) |
63 |
|
fnpr2o |
|- ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o ) |
64 |
4 5 63
|
syl2anc |
|- ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o ) |
65 |
|
dffn5 |
|- ( { <. (/) , R >. , <. 1o , S >. } Fn 2o <-> { <. (/) , R >. , <. 1o , S >. } = ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) |
66 |
64 65
|
sylib |
|- ( ph -> { <. (/) , R >. , <. 1o , S >. } = ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) |
67 |
66
|
oveq2d |
|- ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) |
68 |
67
|
fveq2d |
|- ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( dist ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) |
69 |
67
|
fveq2d |
|- ( ph -> ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) |
70 |
15 69
|
eqtrd |
|- ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) |
71 |
70
|
fveq2d |
|- ( ph -> ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) = ( Met ` ( Base ` ( ( Scalar ` R ) Xs_ ( k e. 2o |-> ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ) ) ) ) |
72 |
62 68 71
|
3eltr4d |
|- ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
73 |
|
ssid |
|- ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
74 |
|
metres2 |
|- ( ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) /\ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
75 |
72 73 74
|
sylancl |
|- ( ph -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
76 |
14 15 18 19 20 6 75
|
imasf1omet |
|- ( ph -> P e. ( Met ` ( X X. Y ) ) ) |