Metamath Proof Explorer

Theorem minveclem3a

Description: Lemma for minvec . D is a complete metric when restricted to Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses minvec.x 
|- X = ( Base ` U )
minvec.m 
|- .- = ( -g ` U )
minvec.n 
|- N = ( norm ` U )
minvec.u 
|- ( ph -> U e. CPreHil )
minvec.y 
|- ( ph -> Y e. ( LSubSp ` U ) )
minvec.w 
|- ( ph -> ( U |`s Y ) e. CMetSp )
minvec.a 
|- ( ph -> A e. X )
minvec.j 
|- J = ( TopOpen ` U )
minvec.r 
|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
minvec.s 
|- S = inf ( R , RR , < )
minvec.d 
|- D = ( ( dist ` U ) |` ( X X. X ) )
Assertion minveclem3a 
|- ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )

Proof

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 ) )