Step |
Hyp |
Ref |
Expression |
1 |
|
minvec.x |
|- X = ( Base ` U ) |
2 |
|
minvec.m |
|- .- = ( -g ` U ) |
3 |
|
minvec.n |
|- N = ( norm ` U ) |
4 |
|
minvec.u |
|- ( ph -> U e. CPreHil ) |
5 |
|
minvec.y |
|- ( ph -> Y e. ( LSubSp ` U ) ) |
6 |
|
minvec.w |
|- ( ph -> ( U |`s Y ) e. CMetSp ) |
7 |
|
minvec.a |
|- ( ph -> A e. X ) |
8 |
|
minvec.j |
|- J = ( TopOpen ` U ) |
9 |
|
minvec.r |
|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) ) |
10 |
|
minvec.s |
|- S = inf ( R , RR , < ) |
11 |
|
minvec.d |
|- D = ( ( dist ` U ) |` ( X X. X ) ) |
12 |
|
eqid |
|- ( Base ` ( U |`s Y ) ) = ( Base ` ( U |`s Y ) ) |
13 |
|
eqid |
|- ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) = ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) |
14 |
12 13
|
cmscmet |
|- ( ( U |`s Y ) e. CMetSp -> ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) e. ( CMet ` ( Base ` ( U |`s Y ) ) ) ) |
15 |
6 14
|
syl |
|- ( ph -> ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) e. ( CMet ` ( Base ` ( U |`s Y ) ) ) ) |
16 |
11
|
reseq1i |
|- ( D |` ( Y X. Y ) ) = ( ( ( dist ` U ) |` ( X X. X ) ) |` ( Y X. Y ) ) |
17 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
18 |
1 17
|
lssss |
|- ( Y e. ( LSubSp ` U ) -> Y C_ X ) |
19 |
5 18
|
syl |
|- ( ph -> Y C_ X ) |
20 |
|
xpss12 |
|- ( ( Y C_ X /\ Y C_ X ) -> ( Y X. Y ) C_ ( X X. X ) ) |
21 |
19 19 20
|
syl2anc |
|- ( ph -> ( Y X. Y ) C_ ( X X. X ) ) |
22 |
21
|
resabs1d |
|- ( ph -> ( ( ( dist ` U ) |` ( X X. X ) ) |` ( Y X. Y ) ) = ( ( dist ` U ) |` ( Y X. Y ) ) ) |
23 |
|
eqid |
|- ( U |`s Y ) = ( U |`s Y ) |
24 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
25 |
23 24
|
ressds |
|- ( Y e. ( LSubSp ` U ) -> ( dist ` U ) = ( dist ` ( U |`s Y ) ) ) |
26 |
5 25
|
syl |
|- ( ph -> ( dist ` U ) = ( dist ` ( U |`s Y ) ) ) |
27 |
23 1
|
ressbas2 |
|- ( Y C_ X -> Y = ( Base ` ( U |`s Y ) ) ) |
28 |
19 27
|
syl |
|- ( ph -> Y = ( Base ` ( U |`s Y ) ) ) |
29 |
28
|
sqxpeqd |
|- ( ph -> ( Y X. Y ) = ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) |
30 |
26 29
|
reseq12d |
|- ( ph -> ( ( dist ` U ) |` ( Y X. Y ) ) = ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) ) |
31 |
22 30
|
eqtrd |
|- ( ph -> ( ( ( dist ` U ) |` ( X X. X ) ) |` ( Y X. Y ) ) = ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) ) |
32 |
16 31
|
syl5eq |
|- ( ph -> ( D |` ( Y X. Y ) ) = ( ( dist ` ( U |`s Y ) ) |` ( ( Base ` ( U |`s Y ) ) X. ( Base ` ( U |`s Y ) ) ) ) ) |
33 |
28
|
fveq2d |
|- ( ph -> ( CMet ` Y ) = ( CMet ` ( Base ` ( U |`s Y ) ) ) ) |
34 |
15 32 33
|
3eltr4d |
|- ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) |