Theorem minveclem6

Description: Lemma for minvec . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

	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	minveclem6	$$⊢\left(\phi \wedge x\in Y\right)\to \left({\left(ADx\right)}^2\le S^2+0\leftrightarrow \forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)\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	11	oveqi	$$⊢ADx=A\left({\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}\right)x$$
13	7	adantr	$$⊢\left(\phi \wedge x\in Y\right)\to A\in X$$
14		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
15	1 14	lssss	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to Y\subseteq X$$
16	5 15	syl	$$⊢\phi \to Y\subseteq X$$
17	16	sselda	$$⊢\left(\phi \wedge x\in Y\right)\to x\in X$$
18	13 17	ovresd	$$⊢\left(\phi \wedge x\in Y\right)\to A\left({\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}\right)x=A\mathrm{dist}\left(U\right)x$$
19	12 18	eqtrid	$$⊢\left(\phi \wedge x\in Y\right)\to ADx=A\mathrm{dist}\left(U\right)x$$
20		cphngp	$$⊢U\in \mathrm{CPreHil}\to U\in \mathrm{NrmGrp}$$
21	4 20	syl	$$⊢\phi \to U\in \mathrm{NrmGrp}$$
22	21	adantr	$$⊢\left(\phi \wedge x\in Y\right)\to U\in \mathrm{NrmGrp}$$
23		eqid	$$⊢\mathrm{dist}\left(U\right)=\mathrm{dist}\left(U\right)$$
24	3 1 2 23	ngpds	$$⊢\left(U\in \mathrm{NrmGrp}\wedge A\in X\wedge x\in X\right)\to A\mathrm{dist}\left(U\right)x=N\left(A\underset{\dot{}}{-}x\right)$$
25	22 13 17 24	syl3anc	$$⊢\left(\phi \wedge x\in Y\right)\to A\mathrm{dist}\left(U\right)x=N\left(A\underset{\dot{}}{-}x\right)$$
26	19 25	eqtrd	$$⊢\left(\phi \wedge x\in Y\right)\to ADx=N\left(A\underset{\dot{}}{-}x\right)$$
27	26	oveq1d	$$⊢\left(\phi \wedge x\in Y\right)\to {\left(ADx\right)}^2={N\left(A\underset{\dot{}}{-}x\right)}^2$$
28	1 2 3 4 5 6 7 8 9	minveclem1	$$⊢\phi \to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\right)$$
29	28	adantr	$$⊢\left(\phi \wedge x\in Y\right)\to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\right)$$
30	29	simp1d	$$⊢\left(\phi \wedge x\in Y\right)\to R\subseteq ℝ$$
31	29	simp2d	$$⊢\left(\phi \wedge x\in Y\right)\to R\ne \varnothing$$
32		0red	$$⊢\left(\phi \wedge x\in Y\right)\to 0\in ℝ$$
33	29	simp3d	$$⊢\left(\phi \wedge x\in Y\right)\to \forall w\in R0\le w$$
34		breq1	$$⊢x=0\to \left(x\le w\leftrightarrow 0\le w\right)$$
35	34	ralbidv	$$⊢x=0\to \left(\forall w\in Rx\le w\leftrightarrow \forall w\in R0\le w\right)$$
36	35	rspcev	$$⊢\left(0\in ℝ\wedge \forall w\in R0\le w\right)\to \exists x\in ℝ\forall w\in Rx\le w$$
37	32 33 36	syl2anc	$$⊢\left(\phi \wedge x\in Y\right)\to \exists x\in ℝ\forall w\in Rx\le w$$
38		infrecl	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists x\in ℝ\forall w\in Rx\le w\right)\to sup\left(R,ℝ,<\right)\in ℝ$$
39	30 31 37 38	syl3anc	$$⊢\left(\phi \wedge x\in Y\right)\to sup\left(R,ℝ,<\right)\in ℝ$$
40	10 39	eqeltrid	$$⊢\left(\phi \wedge x\in Y\right)\to S\in ℝ$$
41	40	resqcld	$$⊢\left(\phi \wedge x\in Y\right)\to S^2\in ℝ$$
42	41	recnd	$$⊢\left(\phi \wedge x\in Y\right)\to S^2\in ℂ$$
43	42	addridd	$$⊢\left(\phi \wedge x\in Y\right)\to S^2+0=S^2$$
44	27 43	breq12d	$$⊢\left(\phi \wedge x\in Y\right)\to \left({\left(ADx\right)}^2\le S^2+0\leftrightarrow {N\left(A\underset{\dot{}}{-}x\right)}^2\le S^2\right)$$
45		cphlmod	$$⊢U\in \mathrm{CPreHil}\to U\in \mathrm{LMod}$$
46	4 45	syl	$$⊢\phi \to U\in \mathrm{LMod}$$
47	46	adantr	$$⊢\left(\phi \wedge x\in Y\right)\to U\in \mathrm{LMod}$$
48	1 2	lmodvsubcl	$$⊢\left(U\in \mathrm{LMod}\wedge A\in X\wedge x\in X\right)\to A\underset{\dot{}}{-}x\in X$$
49	47 13 17 48	syl3anc	$$⊢\left(\phi \wedge x\in Y\right)\to A\underset{\dot{}}{-}x\in X$$
50	1 3	nmcl	$$⊢\left(U\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}x\in X\right)\to N\left(A\underset{\dot{}}{-}x\right)\in ℝ$$
51	22 49 50	syl2anc	$$⊢\left(\phi \wedge x\in Y\right)\to N\left(A\underset{\dot{}}{-}x\right)\in ℝ$$
52	1 3	nmge0	$$⊢\left(U\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}x\in X\right)\to 0\le N\left(A\underset{\dot{}}{-}x\right)$$
53	22 49 52	syl2anc	$$⊢\left(\phi \wedge x\in Y\right)\to 0\le N\left(A\underset{\dot{}}{-}x\right)$$
54		infregelb	$$⊢\left(\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists x\in ℝ\forall w\in Rx\le w\right)\wedge 0\in ℝ\right)\to \left(0\le sup\left(R,ℝ,<\right)\leftrightarrow \forall w\in R0\le w\right)$$
55	30 31 37 32 54	syl31anc	$$⊢\left(\phi \wedge x\in Y\right)\to \left(0\le sup\left(R,ℝ,<\right)\leftrightarrow \forall w\in R0\le w\right)$$
56	33 55	mpbird	$$⊢\left(\phi \wedge x\in Y\right)\to 0\le sup\left(R,ℝ,<\right)$$
57	56 10	breqtrrdi	$$⊢\left(\phi \wedge x\in Y\right)\to 0\le S$$
58	51 40 53 57	le2sqd	$$⊢\left(\phi \wedge x\in Y\right)\to \left(N\left(A\underset{\dot{}}{-}x\right)\le S\leftrightarrow {N\left(A\underset{\dot{}}{-}x\right)}^2\le S^2\right)$$
59	10	breq2i	$$⊢N\left(A\underset{\dot{}}{-}x\right)\le S\leftrightarrow N\left(A\underset{\dot{}}{-}x\right)\le sup\left(R,ℝ,<\right)$$
60		infregelb	$$⊢\left(\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists x\in ℝ\forall w\in Rx\le w\right)\wedge N\left(A\underset{\dot{}}{-}x\right)\in ℝ\right)\to \left(N\left(A\underset{\dot{}}{-}x\right)\le sup\left(R,ℝ,<\right)\leftrightarrow \forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\right)$$
61	30 31 37 51 60	syl31anc	$$⊢\left(\phi \wedge x\in Y\right)\to \left(N\left(A\underset{\dot{}}{-}x\right)\le sup\left(R,ℝ,<\right)\leftrightarrow \forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\right)$$
62	59 61	bitrid	$$⊢\left(\phi \wedge x\in Y\right)\to \left(N\left(A\underset{\dot{}}{-}x\right)\le S\leftrightarrow \forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\right)$$
63	44 58 62	3bitr2d	$$⊢\left(\phi \wedge x\in Y\right)\to \left({\left(ADx\right)}^2\le S^2+0\leftrightarrow \forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\right)$$
64	9	raleqi	$$⊢\forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\leftrightarrow \forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)N\left(A\underset{\dot{}}{-}x\right)\le w$$
65		fvex	$$⊢N\left(A\underset{\dot{}}{-}y\right)\in \mathrm{V}$$
66	65	rgenw	$$⊢\forall y\in YN\left(A\underset{\dot{}}{-}y\right)\in \mathrm{V}$$
67		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)$$
68		breq2	$$⊢w=N\left(A\underset{\dot{}}{-}y\right)\to \left(N\left(A\underset{\dot{}}{-}x\right)\le w\leftrightarrow N\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)\right)$$
69	67 68	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)N\left(A\underset{\dot{}}{-}x\right)\le w\leftrightarrow \forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)\right)$$
70	66 69	ax-mp	$$⊢\forall w\in \mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)N\left(A\underset{\dot{}}{-}x\right)\le w\leftrightarrow \forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)$$
71	64 70	bitri	$$⊢\forall w\in RN\left(A\underset{\dot{}}{-}x\right)\le w\leftrightarrow \forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)$$
72	63 71	bitrdi	$$⊢\left(\phi \wedge x\in Y\right)\to \left({\left(ADx\right)}^2\le S^2+0\leftrightarrow \forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)\right)$$