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={\mathrm{Base}}_U$$
	minvec.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	minvec.n	$$⊢N=\mathrm{norm}\left(U\right)$$
	minvec.u	$$⊢\phi \to U\in \mathrm{CPreHil}$$
	minvec.y	$$⊢\phi \to Y\in \mathrm{LSubSp}\left(U\right)$$
	minvec.w	$$⊢\phi \to U{\upharpoonright }_{𝑠}Y\in \mathrm{CMetSp}$$
	minvec.a	$$⊢\phi \to A\in X$$
	minvec.j	$$⊢J=\mathrm{TopOpen}\left(U\right)$$
	minvec.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
	minvec.s	$$⊢S=sup\left(R,ℝ,<\right)$$
	minvec.d	$$⊢D={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	minveclem3a	$$⊢\phi \to {D\upharpoonright }_{\left(Y\times Y\right)}\in \mathrm{CMet}\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		minvec.x	$$⊢X={\mathrm{Base}}_U$$
2		minvec.m	$$⊢\underset{\dot{}}{-}={-}_U$$
3		minvec.n	$$⊢N=\mathrm{norm}\left(U\right)$$
4		minvec.u	$$⊢\phi \to U\in \mathrm{CPreHil}$$
5		minvec.y	$$⊢\phi \to Y\in \mathrm{LSubSp}\left(U\right)$$
6		minvec.w	$$⊢\phi \to U{\upharpoonright }_{𝑠}Y\in \mathrm{CMetSp}$$
7		minvec.a	$$⊢\phi \to A\in X$$
8		minvec.j	$$⊢J=\mathrm{TopOpen}\left(U\right)$$
9		minvec.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
10		minvec.s	$$⊢S=sup\left(R,ℝ,<\right)$$
11		minvec.d	$$⊢D={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}={\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}$$
13		eqid	$$⊢{\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}={\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}$$
14	12 13	cmscmet	$$⊢U{\upharpoonright }_{𝑠}Y\in \mathrm{CMetSp}\to {\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)$$
15	6 14	syl	$$⊢\phi \to {\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}\in \mathrm{CMet}\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)$$
16	11	reseq1i	$$⊢{D\upharpoonright }_{\left(Y\times Y\right)}={\left({\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}\right)\upharpoonright }_{\left(Y\times Y\right)}$$
17		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
18	1 17	lssss	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to Y\subseteq X$$
19	5 18	syl	$$⊢\phi \to Y\subseteq X$$
20		xpss12	$$⊢\left(Y\subseteq X\wedge Y\subseteq X\right)\to Y\times Y\subseteq X\times X$$
21	19 19 20	syl2anc	$$⊢\phi \to Y\times Y\subseteq X\times X$$
22	21	resabs1d	$$⊢\phi \to {\left({\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}\right)\upharpoonright }_{\left(Y\times Y\right)}={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(Y\times Y\right)}$$
23		eqid	$$⊢U{\upharpoonright }_{𝑠}Y=U{\upharpoonright }_{𝑠}Y$$
24		eqid	$$⊢\mathrm{dist}\left(U\right)=\mathrm{dist}\left(U\right)$$
25	23 24	ressds	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to \mathrm{dist}\left(U\right)=\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)$$
26	5 25	syl	$$⊢\phi \to \mathrm{dist}\left(U\right)=\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)$$
27	23 1	ressbas2	$$⊢Y\subseteq X\to Y={\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}$$
28	19 27	syl	$$⊢\phi \to Y={\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}$$
29	28	sqxpeqd	$$⊢\phi \to Y\times Y={\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}$$
30	26 29	reseq12d	$$⊢\phi \to {\mathrm{dist}\left(U\right)\upharpoonright }_{\left(Y\times Y\right)}={\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}$$
31	22 30	eqtrd	$$⊢\phi \to {\left({\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}\right)\upharpoonright }_{\left(Y\times Y\right)}={\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}$$
32	16 31	eqtrid	$$⊢\phi \to {D\upharpoonright }_{\left(Y\times Y\right)}={\mathrm{dist}\left(U{\upharpoonright }_{𝑠}Y\right)\upharpoonright }_{\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\times {\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)}$$
33	28	fveq2d	$$⊢\phi \to \mathrm{CMet}\left(Y\right)=\mathrm{CMet}\left({\mathrm{Base}}_{\left(U{\upharpoonright }_{𝑠}Y\right)}\right)$$
34	15 32 33	3eltr4d	$$⊢\phi \to {D\upharpoonright }_{\left(Y\times Y\right)}\in \mathrm{CMet}\left(Y\right)$$