minveclem3

Description: Lemma for minvec . The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

	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\})$
Assertion	minveclem3	$⊢ φ \to Y filGen F \in CauFil ({D ↾}_{(Y \times 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		simpr	$⊢ (φ \land s \in ℝ^{+}) \to s \in ℝ^{+}$
14		2z	$⊢ 2 \in ℤ$
15		rpexpcl	$⊢ (s \in ℝ^{+} \land 2 \in ℤ) \to s^{2} \in ℝ^{+}$
16	13 14 15	sylancl	$⊢ (φ \land s \in ℝ^{+}) \to s^{2} \in ℝ^{+}$
17	16	rphalfcld	$⊢ (φ \land s \in ℝ^{+}) \to \frac{s^{2}}{2} \in ℝ^{+}$
18		4nn	$⊢ 4 \in ℕ$
19		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
20	18 19	ax-mp	$⊢ 4 \in ℝ^{+}$
21		rpdivcl	$⊢ (\frac{s^{2}}{2} \in ℝ^{+} \land 4 \in ℝ^{+}) \to \frac{\frac{s^{2}}{2}}{4} \in ℝ^{+}$
22	17 20 21	sylancl	$⊢ (φ \land s \in ℝ^{+}) \to \frac{\frac{s^{2}}{2}}{4} \in ℝ^{+}$
23	5	adantr	$⊢ (φ \land s \in ℝ^{+}) \to Y \in LSubSp (U)$
24		rabexg	$⊢ Y \in LSubSp (U) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in V$
25	23 24	syl	$⊢ (φ \land s \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in V$
26		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\})$
27		oveq2	$⊢ r = \frac{\frac{s^{2}}{2}}{4} \to S^{2} + r = S^{2} + (\frac{\frac{s^{2}}{2}}{4})$
28	27	breq2d	$⊢ r = \frac{\frac{s^{2}}{2}}{4} \to ({(A D y)}^{2} \leq S^{2} + r \leftrightarrow {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}))$
29	28	rabbidv	$⊢ r = \frac{\frac{s^{2}}{2}}{4} \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\}$
30	26 29	elrnmpt1s	$⊢ (\frac{\frac{s^{2}}{2}}{4} \in ℝ^{+} \land \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in V) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
31	22 25 30	syl2anc	$⊢ (φ \land s \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
32	31 12	eleqtrrdi	$⊢ (φ \land s \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in F$
33		oveq2	$⊢ y = u \to A D y = A D u$
34	33	oveq1d	$⊢ y = u \to {(A D y)}^{2} = {(A D u)}^{2}$
35	34	breq1d	$⊢ y = u \to ({(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}) \leftrightarrow {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}))$
36	35	elrab	$⊢ u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \leftrightarrow (u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}))$
37		oveq2	$⊢ y = v \to A D y = A D v$
38	37	oveq1d	$⊢ y = v \to {(A D y)}^{2} = {(A D v)}^{2}$
39	38	breq1d	$⊢ y = v \to ({(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}) \leftrightarrow {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}))$
40	39	elrab	$⊢ v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \leftrightarrow (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4}))$
41	36 40	anbi12i	$⊢ (u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \land v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\}) \leftrightarrow ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))$
42		simprll	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u \in Y$
43		simprrl	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to v \in Y$
44	42 43	ovresd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u ({D ↾}_{(Y \times Y)}) v = u D v$
45		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
46		ngpms	$⊢ U \in NrmGrp \to U \in MetSp$
47	1 11	msmet	$⊢ U \in MetSp \to D \in Met (X)$
48	4 45 46 47	4syl	$⊢ φ \to D \in Met (X)$
49	48	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to D \in Met (X)$
50		eqid	$⊢ LSubSp (U) = LSubSp (U)$
51	1 50	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
52	5 51	syl	$⊢ φ \to Y \subseteq X$
53	52	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to Y \subseteq X$
54	53 42	sseldd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u \in X$
55	53 43	sseldd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to v \in X$
56		metcl	$⊢ (D \in Met (X) \land u \in X \land v \in X) \to u D v \in ℝ$
57	49 54 55 56	syl3anc	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u D v \in ℝ$
58	57	resqcld	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(u D v)}^{2} \in ℝ$
59	17	adantr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{s^{2}}{2} \in ℝ^{+}$
60	59	rpred	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{s^{2}}{2} \in ℝ$
61	16	adantr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to s^{2} \in ℝ^{+}$
62	61	rpred	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to s^{2} \in ℝ$
63	4	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to U \in CPreHil$
64	5	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to Y \in LSubSp (U)$
65	6	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to U ↾_{𝑠} Y \in CMetSp$
66	7	ad2antrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to A \in X$
67	22	adantr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{\frac{s^{2}}{2}}{4} \in ℝ^{+}$
68	67	rpred	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{\frac{s^{2}}{2}}{4} \in ℝ$
69	67	rpge0d	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 0 \leq \frac{\frac{s^{2}}{2}}{4}$
70		simprlr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})$
71		simprrr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})$
72	1 2 3 63 64 65 66 8 9 10 11 68 69 42 43 70 71	minveclem2	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(u D v)}^{2} \leq 4 (\frac{\frac{s^{2}}{2}}{4})$
73	59	rpcnd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{s^{2}}{2} \in ℂ$
74		4cn	$⊢ 4 \in ℂ$
75	74	a1i	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 4 \in ℂ$
76		4ne0	$⊢ 4 \neq 0$
77	76	a1i	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 4 \neq 0$
78	73 75 77	divcan2d	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 4 (\frac{\frac{s^{2}}{2}}{4}) = \frac{s^{2}}{2}$
79	72 78	breqtrd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(u D v)}^{2} \leq \frac{s^{2}}{2}$
80		rphalflt	$⊢ s^{2} \in ℝ^{+} \to \frac{s^{2}}{2} < s^{2}$
81	61 80	syl	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to \frac{s^{2}}{2} < s^{2}$
82	58 60 62 79 81	lelttrd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to {(u D v)}^{2} < s^{2}$
83		rpre	$⊢ s \in ℝ^{+} \to s \in ℝ$
84	83	ad2antlr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to s \in ℝ$
85		metge0	$⊢ (D \in Met (X) \land u \in X \land v \in X) \to 0 \leq u D v$
86	49 54 55 85	syl3anc	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 0 \leq u D v$
87		rpge0	$⊢ s \in ℝ^{+} \to 0 \leq s$
88	87	ad2antlr	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to 0 \leq s$
89	57 84 86 88	lt2sqd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to (u D v < s \leftrightarrow {(u D v)}^{2} < s^{2})$
90	82 89	mpbird	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u D v < s$
91	44 90	eqbrtrd	$⊢ ((φ \land s \in ℝ^{+}) \land ((u \in Y \land {(A D u)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})) \land (v \in Y \land {(A D v)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})))) \to u ({D ↾}_{(Y \times Y)}) v < s$
92	41 91	sylan2b	$⊢ ((φ \land s \in ℝ^{+}) \land (u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \land v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\})) \to u ({D ↾}_{(Y \times Y)}) v < s$
93	92	ralrimivva	$⊢ (φ \land s \in ℝ^{+}) \to \forall u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \forall v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} u ({D ↾}_{(Y \times Y)}) v < s$
94		raleq	$⊢ w = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \to (\forall v \in w u ({D ↾}_{(Y \times Y)}) v < s \leftrightarrow \forall v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} u ({D ↾}_{(Y \times Y)}) v < s)$
95	94	raleqbi1dv	$⊢ w = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \to (\forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s \leftrightarrow \forall u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \forall v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} u ({D ↾}_{(Y \times Y)}) v < s)$
96	95	rspcev	$⊢ (\{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \in F \land \forall u \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} \forall v \in \{y \in Y \| {(A D y)}^{2} \leq S^{2} + (\frac{\frac{s^{2}}{2}}{4})\} u ({D ↾}_{(Y \times Y)}) v < s) \to \exists w \in F \forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s$
97	32 93 96	syl2anc	$⊢ (φ \land s \in ℝ^{+}) \to \exists w \in F \forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s$
98	97	ralrimiva	$⊢ φ \to \forall s \in ℝ^{+} \exists w \in F \forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s$
99	1 2 3 4 5 6 7 8 9 10 11	minveclem3a	$⊢ φ \to {D ↾}_{(Y \times Y)} \in CMet (Y)$
100		cmetmet	$⊢ {D ↾}_{(Y \times Y)} \in CMet (Y) \to {D ↾}_{(Y \times Y)} \in Met (Y)$
101		metxmet	$⊢ {D ↾}_{(Y \times Y)} \in Met (Y) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
102	99 100 101	3syl	$⊢ φ \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
103	1 2 3 4 5 6 7 8 9 10 11 12	minveclem3b	$⊢ φ \to F \in fBas (Y)$
104		fgcfil	$⊢ ({D ↾}_{(Y \times Y)} \in ∞Met (Y) \land F \in fBas (Y)) \to (Y filGen F \in CauFil ({D ↾}_{(Y \times Y)}) \leftrightarrow \forall s \in ℝ^{+} \exists w \in F \forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s)$
105	102 103 104	syl2anc	$⊢ φ \to (Y filGen F \in CauFil ({D ↾}_{(Y \times Y)}) \leftrightarrow \forall s \in ℝ^{+} \exists w \in F \forall u \in w \forall v \in w u ({D ↾}_{(Y \times Y)}) v < s)$
106	98 105	mpbird	$⊢ φ \to Y filGen F \in CauFil ({D ↾}_{(Y \times Y)})$

Metamath Proof Explorer

Theorem minveclem3

Proof