Theorem minveclem1

Description: Lemma for minvec . The set of all distances from points of Y to A are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-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)$$
Assertion	minveclem1	$$⊢\phi \to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\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		cphngp	$$⊢U\in \mathrm{CPreHil}\to U\in \mathrm{NrmGrp}$$
11	4 10	syl	$$⊢\phi \to U\in \mathrm{NrmGrp}$$
12		cphlmod	$$⊢U\in \mathrm{CPreHil}\to U\in \mathrm{LMod}$$
13	4 12	syl	$$⊢\phi \to U\in \mathrm{LMod}$$
14	13	adantr	$$⊢\left(\phi \wedge y\in Y\right)\to U\in \mathrm{LMod}$$
15	7	adantr	$$⊢\left(\phi \wedge y\in Y\right)\to A\in X$$
16		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
17	1 16	lssss	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to Y\subseteq X$$
18	5 17	syl	$$⊢\phi \to Y\subseteq X$$
19	18	sselda	$$⊢\left(\phi \wedge y\in Y\right)\to y\in X$$
20	1 2	lmodvsubcl	$$⊢\left(U\in \mathrm{LMod}\wedge A\in X\wedge y\in X\right)\to A\underset{\dot{}}{-}y\in X$$
21	14 15 19 20	syl3anc	$$⊢\left(\phi \wedge y\in Y\right)\to A\underset{\dot{}}{-}y\in X$$
22	1 3	nmcl	$$⊢\left(U\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}y\in X\right)\to N\left(A\underset{\dot{}}{-}y\right)\in ℝ$$
23	11 21 22	syl2an2r	$$⊢\left(\phi \wedge y\in Y\right)\to N\left(A\underset{\dot{}}{-}y\right)\in ℝ$$
24	23	fmpttd	$$⊢\phi \to \left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right):Y⟶ℝ$$
25	24	frnd	$$⊢\phi \to \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)\subseteq ℝ$$
26	9 25	eqsstrid	$$⊢\phi \to R\subseteq ℝ$$
27	16	lssn0	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to Y\ne \varnothing$$
28	5 27	syl	$$⊢\phi \to Y\ne \varnothing$$
29	9	eqeq1i	$$⊢R=\varnothing \leftrightarrow \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=\varnothing$$
30		dm0rn0	$$⊢\mathrm{dom}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=\varnothing \leftrightarrow \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=\varnothing$$
31		fvex	$$⊢N\left(A\underset{\dot{}}{-}y\right)\in \mathrm{V}$$
32		eqid	$$⊢\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
33	31 32	dmmpti	$$⊢\mathrm{dom}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=Y$$
34	33	eqeq1i	$$⊢\mathrm{dom}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)=\varnothing \leftrightarrow Y=\varnothing$$
35	29 30 34	3bitr2i	$$⊢R=\varnothing \leftrightarrow Y=\varnothing$$
36	35	necon3bii	$$⊢R\ne \varnothing \leftrightarrow Y\ne \varnothing$$
37	28 36	sylibr	$$⊢\phi \to R\ne \varnothing$$
38	1 3	nmge0	$$⊢\left(U\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}y\in X\right)\to 0\le N\left(A\underset{\dot{}}{-}y\right)$$
39	11 21 38	syl2an2r	$$⊢\left(\phi \wedge y\in Y\right)\to 0\le N\left(A\underset{\dot{}}{-}y\right)$$
40	39	ralrimiva	$$⊢\phi \to \forall y\in Y0\le N\left(A\underset{\dot{}}{-}y\right)$$
41	31	rgenw	$$⊢\forall y\in YN\left(A\underset{\dot{}}{-}y\right)\in \mathrm{V}$$
42		breq2	$$⊢w=N\left(A\underset{\dot{}}{-}y\right)\to \left(0\le w\leftrightarrow 0\le N\left(A\underset{\dot{}}{-}y\right)\right)$$
43	32 42	ralrnmptw	$$⊢\forall y\in YN\left(A\underset{\dot{}}{-}y\right)\in \mathrm{V}\to \left(\forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)0\le w\leftrightarrow \forall y\in Y0\le N\left(A\underset{\dot{}}{-}y\right)\right)$$
44	41 43	ax-mp	$$⊢\forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)0\le w\leftrightarrow \forall y\in Y0\le N\left(A\underset{\dot{}}{-}y\right)$$
45	40 44	sylibr	$$⊢\phi \to \forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)0\le w$$
46	9	raleqi	$$⊢\forall w\in R0\le w\leftrightarrow \forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)0\le w$$
47	45 46	sylibr	$$⊢\phi \to \forall w\in R0\le w$$
48	26 37 47	3jca	$$⊢\phi \to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\right)$$