minveclem4a

Description: Lemma for minvec . F converges to a point P in Y . (Contributed by Mario Carneiro, 7-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 = inf (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))$
Assertion	minveclem4a	$⊢ φ \to P \in ((J fLim (X filGen F)) \cap 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 = inf (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		ovex	$⊢ J fLim (X filGen F) \in V$
15	14	uniex	$⊢ ⋃ (J fLim (X filGen F)) \in V$
16	15	snid	$⊢ ⋃ (J fLim (X filGen F)) \in \{⋃ (J fLim (X filGen F))\}$
17		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
18		ngpxms	$⊢ U \in NrmGrp \to U \in ∞MetSp$
19	4 17 18	3syl	$⊢ φ \to U \in ∞MetSp$
20	8 1 11	xmstopn	$⊢ U \in ∞MetSp \to J = MetOpen (D)$
21	19 20	syl	$⊢ φ \to J = MetOpen (D)$
22	21	oveq1d	$⊢ φ \to J ↾_{𝑡} Y = MetOpen (D) ↾_{𝑡} Y$
23	1 11	xmsxmet	$⊢ U \in ∞MetSp \to D \in ∞Met (X)$
24	19 23	syl	$⊢ φ \to D \in ∞Met (X)$
25		eqid	$⊢ LSubSp (U) = LSubSp (U)$
26	1 25	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
27	5 26	syl	$⊢ φ \to Y \subseteq X$
28		eqid	$⊢ {D ↾}_{(Y \times Y)} = {D ↾}_{(Y \times Y)}$
29		eqid	$⊢ MetOpen (D) = MetOpen (D)$
30		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
31	28 29 30	metrest	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to MetOpen (D) ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
32	24 27 31	syl2anc	$⊢ φ \to MetOpen (D) ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
33	22 32	eqtr2d	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) = J ↾_{𝑡} Y$
34	1 2 3 4 5 6 7 8 9 10 11 12	minveclem3b	$⊢ φ \to F \in fBas (Y)$
35		fgcl	$⊢ F \in fBas (Y) \to Y filGen F \in Fil (Y)$
36	34 35	syl	$⊢ φ \to Y filGen F \in Fil (Y)$
37	1	fvexi	$⊢ X \in V$
38	37	a1i	$⊢ φ \to X \in V$
39		trfg	$⊢ (Y filGen F \in Fil (Y) \land Y \subseteq X \land X \in V) \to (X filGen (Y filGen F)) ↾_{𝑡} Y = Y filGen F$
40	36 27 38 39	syl3anc	$⊢ φ \to (X filGen (Y filGen F)) ↾_{𝑡} Y = Y filGen F$
41		fgabs	$⊢ (F \in fBas (Y) \land Y \subseteq X) \to X filGen (Y filGen F) = X filGen F$
42	34 27 41	syl2anc	$⊢ φ \to X filGen (Y filGen F) = X filGen F$
43	42	oveq1d	$⊢ φ \to (X filGen (Y filGen F)) ↾_{𝑡} Y = (X filGen F) ↾_{𝑡} Y$
44	40 43	eqtr3d	$⊢ φ \to Y filGen F = (X filGen F) ↾_{𝑡} Y$
45	33 44	oveq12d	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (Y filGen F) = (J ↾_{𝑡} Y) fLim ((X filGen F) ↾_{𝑡} Y)$
46		xmstps	$⊢ U \in ∞MetSp \to U \in TopSp$
47	19 46	syl	$⊢ φ \to U \in TopSp$
48	1 8	istps	$⊢ U \in TopSp \leftrightarrow J \in TopOn (X)$
49	47 48	sylib	$⊢ φ \to J \in TopOn (X)$
50		fbsspw	$⊢ F \in fBas (Y) \to F \subseteq 𝒫 Y$
51	34 50	syl	$⊢ φ \to F \subseteq 𝒫 Y$
52	27	sspwd	$⊢ φ \to 𝒫 Y \subseteq 𝒫 X$
53	51 52	sstrd	$⊢ φ \to F \subseteq 𝒫 X$
54		fbasweak	$⊢ (F \in fBas (Y) \land F \subseteq 𝒫 X \land X \in V) \to F \in fBas (X)$
55	34 53 38 54	syl3anc	$⊢ φ \to F \in fBas (X)$
56		fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$
57	55 56	syl	$⊢ φ \to X filGen F \in Fil (X)$
58		filfbas	$⊢ Y filGen F \in Fil (Y) \to Y filGen F \in fBas (Y)$
59	34 35 58	3syl	$⊢ φ \to Y filGen F \in fBas (Y)$
60		fbsspw	$⊢ Y filGen F \in fBas (Y) \to Y filGen F \subseteq 𝒫 Y$
61	59 60	syl	$⊢ φ \to Y filGen F \subseteq 𝒫 Y$
62	61 52	sstrd	$⊢ φ \to Y filGen F \subseteq 𝒫 X$
63		fbasweak	$⊢ (Y filGen F \in fBas (Y) \land Y filGen F \subseteq 𝒫 X \land X \in V) \to Y filGen F \in fBas (X)$
64	59 62 38 63	syl3anc	$⊢ φ \to Y filGen F \in fBas (X)$
65		ssfg	$⊢ Y filGen F \in fBas (X) \to Y filGen F \subseteq X filGen (Y filGen F)$
66	64 65	syl	$⊢ φ \to Y filGen F \subseteq X filGen (Y filGen F)$
67	66 42	sseqtrd	$⊢ φ \to Y filGen F \subseteq X filGen F$
68		filtop	$⊢ Y filGen F \in Fil (Y) \to Y \in (Y filGen F)$
69	36 68	syl	$⊢ φ \to Y \in (Y filGen F)$
70	67 69	sseldd	$⊢ φ \to Y \in (X filGen F)$
71		flimrest	$⊢ (J \in TopOn (X) \land X filGen F \in Fil (X) \land Y \in (X filGen F)) \to (J ↾_{𝑡} Y) fLim ((X filGen F) ↾_{𝑡} Y) = (J fLim (X filGen F)) \cap Y$
72	49 57 70 71	syl3anc	$⊢ φ \to (J ↾_{𝑡} Y) fLim ((X filGen F) ↾_{𝑡} Y) = (J fLim (X filGen F)) \cap Y$
73	45 72	eqtrd	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (Y filGen F) = (J fLim (X filGen F)) \cap Y$
74	1 2 3 4 5 6 7 8 9 10 11	minveclem3a	$⊢ φ \to {D ↾}_{(Y \times Y)} \in CMet (Y)$
75	1 2 3 4 5 6 7 8 9 10 11 12	minveclem3	$⊢ φ \to Y filGen F \in CauFil ({D ↾}_{(Y \times Y)})$
76	30	cmetcvg	$⊢ ({D ↾}_{(Y \times Y)} \in CMet (Y) \land Y filGen F \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (Y filGen F) \neq \emptyset$
77	74 75 76	syl2anc	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (Y filGen F) \neq \emptyset$
78	73 77	eqnetrrd	$⊢ φ \to (J fLim (X filGen F)) \cap Y \neq \emptyset$
79	78	neneqd	$⊢ φ \to \neg (J fLim (X filGen F)) \cap Y = \emptyset$
80		inss1	$⊢ (J fLim (X filGen F)) \cap Y \subseteq J fLim (X filGen F)$
81	29	methaus	$⊢ D \in ∞Met (X) \to MetOpen (D) \in Haus$
82	23 81	syl	$⊢ U \in ∞MetSp \to MetOpen (D) \in Haus$
83	20 82	eqeltrd	$⊢ U \in ∞MetSp \to J \in Haus$
84		hausflimi	$⊢ J \in Haus \to \exists^{*} x x \in (J fLim (X filGen F))$
85	19 83 84	3syl	$⊢ φ \to \exists^{*} x x \in (J fLim (X filGen F))$
86		ssn0	$⊢ ((J fLim (X filGen F)) \cap Y \subseteq J fLim (X filGen F) \land (J fLim (X filGen F)) \cap Y \neq \emptyset) \to J fLim (X filGen F) \neq \emptyset$
87	80 78 86	sylancr	$⊢ φ \to J fLim (X filGen F) \neq \emptyset$
88		n0moeu	$⊢ J fLim (X filGen F) \neq \emptyset \to (\exists^{*} x x \in (J fLim (X filGen F)) \leftrightarrow \exists! x x \in (J fLim (X filGen F)))$
89	87 88	syl	$⊢ φ \to (\exists^{*} x x \in (J fLim (X filGen F)) \leftrightarrow \exists! x x \in (J fLim (X filGen F)))$
90	85 89	mpbid	$⊢ φ \to \exists! x x \in (J fLim (X filGen F))$
91		euen1b	$⊢ (J fLim (X filGen F)) \approx 1_{𝑜} \leftrightarrow \exists! x x \in (J fLim (X filGen F))$
92	90 91	sylibr	$⊢ φ \to (J fLim (X filGen F)) \approx 1_{𝑜}$
93		en1b	$⊢ (J fLim (X filGen F)) \approx 1_{𝑜} \leftrightarrow J fLim (X filGen F) = \{⋃ (J fLim (X filGen F))\}$
94	92 93	sylib	$⊢ φ \to J fLim (X filGen F) = \{⋃ (J fLim (X filGen F))\}$
95	80 94	sseqtrid	$⊢ φ \to (J fLim (X filGen F)) \cap Y \subseteq \{⋃ (J fLim (X filGen F))\}$
96		sssn	$⊢ (J fLim (X filGen F)) \cap Y \subseteq \{⋃ (J fLim (X filGen F))\} \leftrightarrow ((J fLim (X filGen F)) \cap Y = \emptyset \lor (J fLim (X filGen F)) \cap Y = \{⋃ (J fLim (X filGen F))\})$
97	95 96	sylib	$⊢ φ \to ((J fLim (X filGen F)) \cap Y = \emptyset \lor (J fLim (X filGen F)) \cap Y = \{⋃ (J fLim (X filGen F))\})$
98	97	ord	$⊢ φ \to (\neg (J fLim (X filGen F)) \cap Y = \emptyset \to (J fLim (X filGen F)) \cap Y = \{⋃ (J fLim (X filGen F))\})$
99	79 98	mpd	$⊢ φ \to (J fLim (X filGen F)) \cap Y = \{⋃ (J fLim (X filGen F))\}$
100	16 99	eleqtrrid	$⊢ φ \to ⋃ (J fLim (X filGen F)) \in ((J fLim (X filGen F)) \cap Y)$
101	13 100	eqeltrid	$⊢ φ \to P \in ((J fLim (X filGen F)) \cap Y)$

Metamath Proof Explorer

Theorem minveclem4a

Proof