minveclem4

Description: Lemma for minvec . The convergent point of the Cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	minvec.x	$⊢ X = {Base}_{U}$
	minvec.m	$⊢ \underset{˙}{-} = -_{U}$
	minvec.n	$⊢ N = norm (U)$
	minvec.u	$⊢ φ \to U \in CPreHil$
	minvec.y	$⊢ φ \to Y \in LSubSp (U)$
	minvec.w	$⊢ φ \to U ↾_{𝑠} Y \in CMetSp$
	minvec.a	$⊢ φ \to A \in X$
	minvec.j	$⊢ J = TopOpen (U)$
	minvec.r	$⊢ R = ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
	minvec.s	$⊢ S = sup (R ℝ <)$
	minvec.d	$⊢ D = {dist (U) ↾}_{(X \times X)}$
	minvec.f	$⊢ F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
	minvec.p	$⊢ P = ⋃ (J fLim (X filGen F))$
	minvec.t	$⊢ T = {(\frac{(A D P) + S}{2})}^{2} - S^{2}$
Assertion	minveclem4	$⊢ φ \to \exists x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$

Proof

Step	Hyp	Ref	Expression
1		minvec.x	$⊢ X = {Base}_{U}$
2		minvec.m	$⊢ \underset{˙}{-} = -_{U}$
3		minvec.n	$⊢ N = norm (U)$
4		minvec.u	$⊢ φ \to U \in CPreHil$
5		minvec.y	$⊢ φ \to Y \in LSubSp (U)$
6		minvec.w	$⊢ φ \to U ↾_{𝑠} Y \in CMetSp$
7		minvec.a	$⊢ φ \to A \in X$
8		minvec.j	$⊢ J = TopOpen (U)$
9		minvec.r	$⊢ R = ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
10		minvec.s	$⊢ S = sup (R ℝ <)$
11		minvec.d	$⊢ D = {dist (U) ↾}_{(X \times X)}$
12		minvec.f	$⊢ F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
13		minvec.p	$⊢ P = ⋃ (J fLim (X filGen F))$
14		minvec.t	$⊢ T = {(\frac{(A D P) + S}{2})}^{2} - S^{2}$
15	1 2 3 4 5 6 7 8 9 10 11 12 13	minveclem4a	$⊢ φ \to P \in ((J fLim (X filGen F)) \cap Y)$
16	15	elin2d	$⊢ φ \to P \in Y$
17	11	oveqi	$⊢ A D P = A ({dist (U) ↾}_{(X \times X)}) P$
18	1 2 3 4 5 6 7 8 9 10 11 12 13	minveclem4b	$⊢ φ \to P \in X$
19	7 18	ovresd	$⊢ φ \to A ({dist (U) ↾}_{(X \times X)}) P = A dist (U) P$
20	17 19	eqtrid	$⊢ φ \to A D P = A dist (U) P$
21		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
22	4 21	syl	$⊢ φ \to U \in NrmGrp$
23		eqid	$⊢ dist (U) = dist (U)$
24	3 1 2 23	ngpds	$⊢ (U \in NrmGrp \land A \in X \land P \in X) \to A dist (U) P = N (A \underset{˙}{-} P)$
25	22 7 18 24	syl3anc	$⊢ φ \to A dist (U) P = N (A \underset{˙}{-} P)$
26	20 25	eqtrd	$⊢ φ \to A D P = N (A \underset{˙}{-} P)$
27	26	adantr	$⊢ (φ \land y \in Y) \to A D P = N (A \underset{˙}{-} P)$
28		ngpms	$⊢ U \in NrmGrp \to U \in MetSp$
29	1 11	msmet	$⊢ U \in MetSp \to D \in Met (X)$
30	22 28 29	3syl	$⊢ φ \to D \in Met (X)$
31		metcl	$⊢ (D \in Met (X) \land A \in X \land P \in X) \to A D P \in ℝ$
32	30 7 18 31	syl3anc	$⊢ φ \to A D P \in ℝ$
33	32	adantr	$⊢ (φ \land y \in Y) \to A D P \in ℝ$
34	1 2 3 4 5 6 7 8 9 10	minveclem4c	$⊢ φ \to S \in ℝ$
35	34	adantr	$⊢ (φ \land y \in Y) \to S \in ℝ$
36	22	adantr	$⊢ (φ \land y \in Y) \to U \in NrmGrp$
37		cphlmod	$⊢ U \in CPreHil \to U \in LMod$
38	4 37	syl	$⊢ φ \to U \in LMod$
39	38	adantr	$⊢ (φ \land y \in Y) \to U \in LMod$
40	7	adantr	$⊢ (φ \land y \in Y) \to A \in X$
41		eqid	$⊢ LSubSp (U) = LSubSp (U)$
42	1 41	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
43	5 42	syl	$⊢ φ \to Y \subseteq X$
44	43	sselda	$⊢ (φ \land y \in Y) \to y \in X$
45	1 2	lmodvsubcl	$⊢ (U \in LMod \land A \in X \land y \in X) \to A \underset{˙}{-} y \in X$
46	39 40 44 45	syl3anc	$⊢ (φ \land y \in Y) \to A \underset{˙}{-} y \in X$
47	1 3	nmcl	$⊢ (U \in NrmGrp \land A \underset{˙}{-} y \in X) \to N (A \underset{˙}{-} y) \in ℝ$
48	36 46 47	syl2anc	$⊢ (φ \land y \in Y) \to N (A \underset{˙}{-} y) \in ℝ$
49	34 32	ltnled	$⊢ φ \to (S < A D P \leftrightarrow \neg A D P \leq S)$
50	1 2 3 4 5 6 7 8 9 10 11 12	minveclem3b	$⊢ φ \to F \in fBas (Y)$
51		fbsspw	$⊢ F \in fBas (Y) \to F \subseteq 𝒫 Y$
52	50 51	syl	$⊢ φ \to F \subseteq 𝒫 Y$
53	43	sspwd	$⊢ φ \to 𝒫 Y \subseteq 𝒫 X$
54	52 53	sstrd	$⊢ φ \to F \subseteq 𝒫 X$
55	1	fvexi	$⊢ X \in V$
56	55	a1i	$⊢ φ \to X \in V$
57		fbasweak	$⊢ (F \in fBas (Y) \land F \subseteq 𝒫 X \land X \in V) \to F \in fBas (X)$
58	50 54 56 57	syl3anc	$⊢ φ \to F \in fBas (X)$
59	58	adantr	$⊢ (φ \land S < A D P) \to F \in fBas (X)$
60		fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$
61	59 60	syl	$⊢ (φ \land S < A D P) \to X filGen F \in Fil (X)$
62		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
63	59 62	syl	$⊢ (φ \land S < A D P) \to F \subseteq X filGen F$
64	32 34	readdcld	$⊢ φ \to (A D P) + S \in ℝ$
65	64	rehalfcld	$⊢ φ \to \frac{(A D P) + S}{2} \in ℝ$
66	65	resqcld	$⊢ φ \to {(\frac{(A D P) + S}{2})}^{2} \in ℝ$
67	34	resqcld	$⊢ φ \to S^{2} \in ℝ$
68	66 67	resubcld	$⊢ φ \to {(\frac{(A D P) + S}{2})}^{2} - S^{2} \in ℝ$
69	68	adantr	$⊢ (φ \land S < A D P) \to {(\frac{(A D P) + S}{2})}^{2} - S^{2} \in ℝ$
70	34 32 34	ltadd1d	$⊢ φ \to (S < A D P \leftrightarrow S + S < (A D P) + S)$
71	34	recnd	$⊢ φ \to S \in ℂ$
72	71	2timesd	$⊢ φ \to 2 S = S + S$
73	72	breq1d	$⊢ φ \to (2 S < (A D P) + S \leftrightarrow S + S < (A D P) + S)$
74		2re	$⊢ 2 \in ℝ$
75		2pos	$⊢ 0 < 2$
76	74 75	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
77	76	a1i	$⊢ φ \to (2 \in ℝ \land 0 < 2)$
78		ltmuldiv2	$⊢ (S \in ℝ \land (A D P) + S \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 S < (A D P) + S \leftrightarrow S < \frac{(A D P) + S}{2})$
79	34 64 77 78	syl3anc	$⊢ φ \to (2 S < (A D P) + S \leftrightarrow S < \frac{(A D P) + S}{2})$
80	70 73 79	3bitr2d	$⊢ φ \to (S < A D P \leftrightarrow S < \frac{(A D P) + S}{2})$
81	1 2 3 4 5 6 7 8 9	minveclem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
82	81	simp3d	$⊢ φ \to \forall w \in R 0 \leq w$
83	81	simp1d	$⊢ φ \to R \subseteq ℝ$
84	81	simp2d	$⊢ φ \to R \neq \emptyset$
85		0re	$⊢ 0 \in ℝ$
86		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
87	86	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
88	87	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
89	85 82 88	sylancr	$⊢ φ \to \exists x \in ℝ \forall w \in R x \leq w$
90	85	a1i	$⊢ φ \to 0 \in ℝ$
91		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land 0 \in ℝ) \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
92	83 84 89 90 91	syl31anc	$⊢ φ \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
93	82 92	mpbird	$⊢ φ \to 0 \leq sup (R ℝ <)$
94	93 10	breqtrrdi	$⊢ φ \to 0 \leq S$
95		metge0	$⊢ (D \in Met (X) \land A \in X \land P \in X) \to 0 \leq A D P$
96	30 7 18 95	syl3anc	$⊢ φ \to 0 \leq A D P$
97	32 34 96 94	addge0d	$⊢ φ \to 0 \leq (A D P) + S$
98		divge0	$⊢ (((A D P) + S \in ℝ \land 0 \leq (A D P) + S) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{(A D P) + S}{2}$
99	64 97 77 98	syl21anc	$⊢ φ \to 0 \leq \frac{(A D P) + S}{2}$
100	34 65 94 99	lt2sqd	$⊢ φ \to (S < \frac{(A D P) + S}{2} \leftrightarrow S^{2} < {(\frac{(A D P) + S}{2})}^{2})$
101	67 66	posdifd	$⊢ φ \to (S^{2} < {(\frac{(A D P) + S}{2})}^{2} \leftrightarrow 0 < {(\frac{(A D P) + S}{2})}^{2} - S^{2})$
102	80 100 101	3bitrd	$⊢ φ \to (S < A D P \leftrightarrow 0 < {(\frac{(A D P) + S}{2})}^{2} - S^{2})$
103	102	biimpa	$⊢ (φ \land S < A D P) \to 0 < {(\frac{(A D P) + S}{2})}^{2} - S^{2}$
104	69 103	elrpd	$⊢ (φ \land S < A D P) \to {(\frac{(A D P) + S}{2})}^{2} - S^{2} \in ℝ^{+}$
105	14 104	eqeltrid	$⊢ (φ \land S < A D P) \to T \in ℝ^{+}$
106	5	adantr	$⊢ (φ \land S < A D P) \to Y \in LSubSp (U)$
107		rabexg	$⊢ Y \in LSubSp (U) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in V$
108	106 107	syl	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in V$
109		eqid	$⊢ (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
110		oveq2	$⊢ r = T \to S^{2} + r = S^{2} + T$
111	110	breq2d	$⊢ r = T \to ({(A D y)}^{2} \leq S^{2} + r \leftrightarrow {(A D y)}^{2} \leq S^{2} + T)$
112	111	rabbidv	$⊢ r = T \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\}$
113	109 112	elrnmpt1s	$⊢ (T \in ℝ^{+} \land \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in V) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
114	105 108 113	syl2anc	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
115	114 12	eleqtrrdi	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in F$
116	63 115	sseldd	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in (X filGen F)$
117		ssrab2	$⊢ \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \subseteq X$
118	117	a1i	$⊢ (φ \land S < A D P) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \subseteq X$
119	14	oveq2i	$⊢ S^{2} + T = S^{2} + {(\frac{(A D P) + S}{2})}^{2} - S^{2}$
120	67	ad2antrr	$⊢ ((φ \land S < A D P) \land y \in Y) \to S^{2} \in ℝ$
121	120	recnd	$⊢ ((φ \land S < A D P) \land y \in Y) \to S^{2} \in ℂ$
122	65	ad2antrr	$⊢ ((φ \land S < A D P) \land y \in Y) \to \frac{(A D P) + S}{2} \in ℝ$
123	122	resqcld	$⊢ ((φ \land S < A D P) \land y \in Y) \to {(\frac{(A D P) + S}{2})}^{2} \in ℝ$
124	123	recnd	$⊢ ((φ \land S < A D P) \land y \in Y) \to {(\frac{(A D P) + S}{2})}^{2} \in ℂ$
125	121 124	pncan3d	$⊢ ((φ \land S < A D P) \land y \in Y) \to S^{2} + {(\frac{(A D P) + S}{2})}^{2} - S^{2} = {(\frac{(A D P) + S}{2})}^{2}$
126	119 125	eqtrid	$⊢ ((φ \land S < A D P) \land y \in Y) \to S^{2} + T = {(\frac{(A D P) + S}{2})}^{2}$
127	126	breq2d	$⊢ ((φ \land S < A D P) \land y \in Y) \to ({(A D y)}^{2} \leq S^{2} + T \leftrightarrow {(A D y)}^{2} \leq {(\frac{(A D P) + S}{2})}^{2})$
128	30	ad2antrr	$⊢ ((φ \land S < A D P) \land y \in Y) \to D \in Met (X)$
129	7	ad2antrr	$⊢ ((φ \land S < A D P) \land y \in Y) \to A \in X$
130	44	adantlr	$⊢ ((φ \land S < A D P) \land y \in Y) \to y \in X$
131		metcl	$⊢ (D \in Met (X) \land A \in X \land y \in X) \to A D y \in ℝ$
132	128 129 130 131	syl3anc	$⊢ ((φ \land S < A D P) \land y \in Y) \to A D y \in ℝ$
133		metge0	$⊢ (D \in Met (X) \land A \in X \land y \in X) \to 0 \leq A D y$
134	128 129 130 133	syl3anc	$⊢ ((φ \land S < A D P) \land y \in Y) \to 0 \leq A D y$
135	99	ad2antrr	$⊢ ((φ \land S < A D P) \land y \in Y) \to 0 \leq \frac{(A D P) + S}{2}$
136	132 122 134 135	le2sqd	$⊢ ((φ \land S < A D P) \land y \in Y) \to (A D y \leq \frac{(A D P) + S}{2} \leftrightarrow {(A D y)}^{2} \leq {(\frac{(A D P) + S}{2})}^{2})$
137	127 136	bitr4d	$⊢ ((φ \land S < A D P) \land y \in Y) \to ({(A D y)}^{2} \leq S^{2} + T \leftrightarrow A D y \leq \frac{(A D P) + S}{2})$
138	137	rabbidva	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} = \{y \in Y \| A D y \leq \frac{(A D P) + S}{2}\}$
139	43	adantr	$⊢ (φ \land S < A D P) \to Y \subseteq X$
140		rabss2	$⊢ Y \subseteq X \to \{y \in Y \| A D y \leq \frac{(A D P) + S}{2}\} \subseteq \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
141	139 140	syl	$⊢ (φ \land S < A D P) \to \{y \in Y \| A D y \leq \frac{(A D P) + S}{2}\} \subseteq \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
142	138 141	eqsstrd	$⊢ (φ \land S < A D P) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \subseteq \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
143		filss	$⊢ (X filGen F \in Fil (X) \land (\{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \in (X filGen F) \land \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \subseteq X \land \{y \in Y \| {(A D y)}^{2} \leq S^{2} + T\} \subseteq \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\})) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in (X filGen F)$
144	61 116 118 142 143	syl13anc	$⊢ (φ \land S < A D P) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in (X filGen F)$
145		flimclsi	$⊢ \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in (X filGen F) \to J fLim (X filGen F) \subseteq cls (J) (\{y \in X \| A D y \leq \frac{(A D P) + S}{2}\})$
146	144 145	syl	$⊢ (φ \land S < A D P) \to J fLim (X filGen F) \subseteq cls (J) (\{y \in X \| A D y \leq \frac{(A D P) + S}{2}\})$
147	15	elin1d	$⊢ φ \to P \in (J fLim (X filGen F))$
148	147	adantr	$⊢ (φ \land S < A D P) \to P \in (J fLim (X filGen F))$
149	146 148	sseldd	$⊢ (φ \land S < A D P) \to P \in cls (J) (\{y \in X \| A D y \leq \frac{(A D P) + S}{2}\})$
150		ngpxms	$⊢ U \in NrmGrp \to U \in ∞MetSp$
151	1 11	xmsxmet	$⊢ U \in ∞MetSp \to D \in ∞Met (X)$
152	22 150 151	3syl	$⊢ φ \to D \in ∞Met (X)$
153	152	adantr	$⊢ (φ \land S < A D P) \to D \in ∞Met (X)$
154	7	adantr	$⊢ (φ \land S < A D P) \to A \in X$
155	65	adantr	$⊢ (φ \land S < A D P) \to \frac{(A D P) + S}{2} \in ℝ$
156	155	rexrd	$⊢ (φ \land S < A D P) \to \frac{(A D P) + S}{2} \in ℝ^{*}$
157		eqid	$⊢ MetOpen (D) = MetOpen (D)$
158		eqid	$⊢ \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} = \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
159	157 158	blcld	$⊢ (D \in ∞Met (X) \land A \in X \land \frac{(A D P) + S}{2} \in ℝ^{*}) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in Clsd (MetOpen (D))$
160	153 154 156 159	syl3anc	$⊢ (φ \land S < A D P) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in Clsd (MetOpen (D))$
161	8 1 11	xmstopn	$⊢ U \in ∞MetSp \to J = MetOpen (D)$
162	22 150 161	3syl	$⊢ φ \to J = MetOpen (D)$
163	162	adantr	$⊢ (φ \land S < A D P) \to J = MetOpen (D)$
164	163	fveq2d	$⊢ (φ \land S < A D P) \to Clsd (J) = Clsd (MetOpen (D))$
165	160 164	eleqtrrd	$⊢ (φ \land S < A D P) \to \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in Clsd (J)$
166		cldcls	$⊢ \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \in Clsd (J) \to cls (J) (\{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}) = \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
167	165 166	syl	$⊢ (φ \land S < A D P) \to cls (J) (\{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}) = \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
168	149 167	eleqtrd	$⊢ (φ \land S < A D P) \to P \in \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\}$
169		oveq2	$⊢ y = P \to A D y = A D P$
170	169	breq1d	$⊢ y = P \to (A D y \leq \frac{(A D P) + S}{2} \leftrightarrow A D P \leq \frac{(A D P) + S}{2})$
171	170	elrab	$⊢ P \in \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \leftrightarrow (P \in X \land A D P \leq \frac{(A D P) + S}{2})$
172	171	simprbi	$⊢ P \in \{y \in X \| A D y \leq \frac{(A D P) + S}{2}\} \to A D P \leq \frac{(A D P) + S}{2}$
173	168 172	syl	$⊢ (φ \land S < A D P) \to A D P \leq \frac{(A D P) + S}{2}$
174	32 34 32	leadd2d	$⊢ φ \to (A D P \leq S \leftrightarrow (A D P) + (A D P) \leq (A D P) + S)$
175	32	recnd	$⊢ φ \to A D P \in ℂ$
176	175	2timesd	$⊢ φ \to 2 (A D P) = (A D P) + (A D P)$
177	176	breq1d	$⊢ φ \to (2 (A D P) \leq (A D P) + S \leftrightarrow (A D P) + (A D P) \leq (A D P) + S)$
178		lemuldiv2	$⊢ (A D P \in ℝ \land (A D P) + S \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 (A D P) \leq (A D P) + S \leftrightarrow A D P \leq \frac{(A D P) + S}{2})$
179	76 178	mp3an3	$⊢ (A D P \in ℝ \land (A D P) + S \in ℝ) \to (2 (A D P) \leq (A D P) + S \leftrightarrow A D P \leq \frac{(A D P) + S}{2})$
180	32 64 179	syl2anc	$⊢ φ \to (2 (A D P) \leq (A D P) + S \leftrightarrow A D P \leq \frac{(A D P) + S}{2})$
181	174 177 180	3bitr2d	$⊢ φ \to (A D P \leq S \leftrightarrow A D P \leq \frac{(A D P) + S}{2})$
182	181	biimpar	$⊢ (φ \land A D P \leq \frac{(A D P) + S}{2}) \to A D P \leq S$
183	173 182	syldan	$⊢ (φ \land S < A D P) \to A D P \leq S$
184	183	ex	$⊢ φ \to (S < A D P \to A D P \leq S)$
185	49 184	sylbird	$⊢ φ \to (\neg A D P \leq S \to A D P \leq S)$
186	185	pm2.18d	$⊢ φ \to A D P \leq S$
187	186	adantr	$⊢ (φ \land y \in Y) \to A D P \leq S$
188	83	adantr	$⊢ (φ \land y \in Y) \to R \subseteq ℝ$
189	89	adantr	$⊢ (φ \land y \in Y) \to \exists x \in ℝ \forall w \in R x \leq w$
190		simpr	$⊢ (φ \land y \in Y) \to y \in Y$
191		fvex	$⊢ N (A \underset{˙}{-} y) \in V$
192		eqid	$⊢ (y \in Y ⟼ N (A \underset{˙}{-} y)) = (y \in Y ⟼ N (A \underset{˙}{-} y))$
193	192	elrnmpt1	$⊢ (y \in Y \land N (A \underset{˙}{-} y) \in V) \to N (A \underset{˙}{-} y) \in ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
194	190 191 193	sylancl	$⊢ (φ \land y \in Y) \to N (A \underset{˙}{-} y) \in ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
195	194 9	eleqtrrdi	$⊢ (φ \land y \in Y) \to N (A \underset{˙}{-} y) \in R$
196		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall w \in R x \leq w \land N (A \underset{˙}{-} y) \in R) \to sup (R ℝ <) \leq N (A \underset{˙}{-} y)$
197	188 189 195 196	syl3anc	$⊢ (φ \land y \in Y) \to sup (R ℝ <) \leq N (A \underset{˙}{-} y)$
198	10 197	eqbrtrid	$⊢ (φ \land y \in Y) \to S \leq N (A \underset{˙}{-} y)$
199	33 35 48 187 198	letrd	$⊢ (φ \land y \in Y) \to A D P \leq N (A \underset{˙}{-} y)$
200	27 199	eqbrtrrd	$⊢ (φ \land y \in Y) \to N (A \underset{˙}{-} P) \leq N (A \underset{˙}{-} y)$
201	200	ralrimiva	$⊢ φ \to \forall y \in Y N (A \underset{˙}{-} P) \leq N (A \underset{˙}{-} y)$
202		oveq2	$⊢ x = P \to A \underset{˙}{-} x = A \underset{˙}{-} P$
203	202	fveq2d	$⊢ x = P \to N (A \underset{˙}{-} x) = N (A \underset{˙}{-} P)$
204	203	breq1d	$⊢ x = P \to (N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow N (A \underset{˙}{-} P) \leq N (A \underset{˙}{-} y))$
205	204	ralbidv	$⊢ x = P \to (\forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow \forall y \in Y N (A \underset{˙}{-} P) \leq N (A \underset{˙}{-} y))$
206	205	rspcev	$⊢ (P \in Y \land \forall y \in Y N (A \underset{˙}{-} P) \leq N (A \underset{˙}{-} y)) \to \exists x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
207	16 201 206	syl2anc	$⊢ φ \to \exists x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$

Metamath Proof Explorer

Theorem minveclem4

Proof