minveclem3b

Description: Lemma for minvec . The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed 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\})$
Assertion	minveclem3b	$⊢ φ \to F \in fBas (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		ssrab2	$⊢ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \subseteq Y$
14	5	adantr	$⊢ (φ \land r \in ℝ^{+}) \to Y \in LSubSp (U)$
15		elpw2g	$⊢ Y \in LSubSp (U) \to (\{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \in 𝒫 Y \leftrightarrow \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \subseteq Y)$
16	14 15	syl	$⊢ (φ \land r \in ℝ^{+}) \to (\{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \in 𝒫 Y \leftrightarrow \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \subseteq Y)$
17	13 16	mpbiri	$⊢ (φ \land r \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \in 𝒫 Y$
18	17	fmpttd	$⊢ φ \to (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) : ℝ^{+} ⟶ 𝒫 Y$
19	18	frnd	$⊢ φ \to ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) \subseteq 𝒫 Y$
20	12 19	eqsstrid	$⊢ φ \to F \subseteq 𝒫 Y$
21		1rp	$⊢ 1 \in ℝ^{+}$
22		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\})$
23	22 17	dmmptd	$⊢ φ \to dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = ℝ^{+}$
24	21 23	eleqtrrid	$⊢ φ \to 1 \in dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
25	24	ne0d	$⊢ φ \to dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) \neq \emptyset$
26		dm0rn0	$⊢ dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = \emptyset \leftrightarrow ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = \emptyset$
27	12	eqeq1i	$⊢ F = \emptyset \leftrightarrow ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = \emptyset$
28	26 27	bitr4i	$⊢ dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) = \emptyset \leftrightarrow F = \emptyset$
29	28	necon3bii	$⊢ dom (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) \neq \emptyset \leftrightarrow F \neq \emptyset$
30	25 29	sylib	$⊢ φ \to F \neq \emptyset$
31	1 2 3 4 5 6 7 8 9 10	minveclem4c	$⊢ φ \to S \in ℝ$
32	31	resqcld	$⊢ φ \to S^{2} \in ℝ$
33		ltaddrp	$⊢ (S^{2} \in ℝ \land r \in ℝ^{+}) \to S^{2} < S^{2} + r$
34	32 33	sylan	$⊢ (φ \land r \in ℝ^{+}) \to S^{2} < S^{2} + r$
35	32	adantr	$⊢ (φ \land r \in ℝ^{+}) \to S^{2} \in ℝ$
36		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
37	36	adantl	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ$
38	35 37	readdcld	$⊢ (φ \land r \in ℝ^{+}) \to S^{2} + r \in ℝ$
39	38	recnd	$⊢ (φ \land r \in ℝ^{+}) \to S^{2} + r \in ℂ$
40	39	sqsqrtd	$⊢ (φ \land r \in ℝ^{+}) \to {\sqrt{S^{2} + r}}^{2} = S^{2} + r$
41	34 40	breqtrrd	$⊢ (φ \land r \in ℝ^{+}) \to S^{2} < {\sqrt{S^{2} + r}}^{2}$
42	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)$
43	42	simp1d	$⊢ φ \to R \subseteq ℝ$
44	43	adantr	$⊢ (φ \land r \in ℝ^{+}) \to R \subseteq ℝ$
45	42	simp2d	$⊢ φ \to R \neq \emptyset$
46	45	adantr	$⊢ (φ \land r \in ℝ^{+}) \to R \neq \emptyset$
47		0re	$⊢ 0 \in ℝ$
48	42	simp3d	$⊢ φ \to \forall w \in R 0 \leq w$
49		breq1	$⊢ y = 0 \to (y \leq w \leftrightarrow 0 \leq w)$
50	49	ralbidv	$⊢ y = 0 \to (\forall w \in R y \leq w \leftrightarrow \forall w \in R 0 \leq w)$
51	50	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists y \in ℝ \forall w \in R y \leq w$
52	47 48 51	sylancr	$⊢ φ \to \exists y \in ℝ \forall w \in R y \leq w$
53	52	adantr	$⊢ (φ \land r \in ℝ^{+}) \to \exists y \in ℝ \forall w \in R y \leq w$
54		infrecl	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \exists y \in ℝ \forall w \in R y \leq w) \to sup (R ℝ <) \in ℝ$
55	44 46 53 54	syl3anc	$⊢ (φ \land r \in ℝ^{+}) \to sup (R ℝ <) \in ℝ$
56	10 55	eqeltrid	$⊢ (φ \land r \in ℝ^{+}) \to S \in ℝ$
57		0red	$⊢ (φ \land r \in ℝ^{+}) \to 0 \in ℝ$
58	56	sqge0d	$⊢ (φ \land r \in ℝ^{+}) \to 0 \leq S^{2}$
59	57 35 38 58 34	lelttrd	$⊢ (φ \land r \in ℝ^{+}) \to 0 < S^{2} + r$
60	57 38 59	ltled	$⊢ (φ \land r \in ℝ^{+}) \to 0 \leq S^{2} + r$
61	38 60	resqrtcld	$⊢ (φ \land r \in ℝ^{+}) \to \sqrt{S^{2} + r} \in ℝ$
62	48	adantr	$⊢ (φ \land r \in ℝ^{+}) \to \forall w \in R 0 \leq w$
63		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists y \in ℝ \forall w \in R y \leq w) \land 0 \in ℝ) \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
64	44 46 53 57 63	syl31anc	$⊢ (φ \land r \in ℝ^{+}) \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
65	62 64	mpbird	$⊢ (φ \land r \in ℝ^{+}) \to 0 \leq sup (R ℝ <)$
66	65 10	breqtrrdi	$⊢ (φ \land r \in ℝ^{+}) \to 0 \leq S$
67	38 60	sqrtge0d	$⊢ (φ \land r \in ℝ^{+}) \to 0 \leq \sqrt{S^{2} + r}$
68	56 61 66 67	lt2sqd	$⊢ (φ \land r \in ℝ^{+}) \to (S < \sqrt{S^{2} + r} \leftrightarrow S^{2} < {\sqrt{S^{2} + r}}^{2})$
69	41 68	mpbird	$⊢ (φ \land r \in ℝ^{+}) \to S < \sqrt{S^{2} + r}$
70	56 61	ltnled	$⊢ (φ \land r \in ℝ^{+}) \to (S < \sqrt{S^{2} + r} \leftrightarrow \neg \sqrt{S^{2} + r} \leq S)$
71	69 70	mpbid	$⊢ (φ \land r \in ℝ^{+}) \to \neg \sqrt{S^{2} + r} \leq S$
72	10	breq2i	$⊢ \sqrt{S^{2} + r} \leq S \leftrightarrow \sqrt{S^{2} + r} \leq sup (R ℝ <)$
73		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists y \in ℝ \forall w \in R y \leq w) \land \sqrt{S^{2} + r} \in ℝ) \to (\sqrt{S^{2} + r} \leq sup (R ℝ <) \leftrightarrow \forall w \in R \sqrt{S^{2} + r} \leq w)$
74	44 46 53 61 73	syl31anc	$⊢ (φ \land r \in ℝ^{+}) \to (\sqrt{S^{2} + r} \leq sup (R ℝ <) \leftrightarrow \forall w \in R \sqrt{S^{2} + r} \leq w)$
75	9	raleqi	$⊢ \forall w \in R \sqrt{S^{2} + r} \leq w \leftrightarrow \forall w \in ran (y \in Y ⟼ N (A \underset{˙}{-} y)) \sqrt{S^{2} + r} \leq w$
76		fvex	$⊢ N (A \underset{˙}{-} y) \in V$
77	76	rgenw	$⊢ \forall y \in Y N (A \underset{˙}{-} y) \in V$
78		eqid	$⊢ (y \in Y ⟼ N (A \underset{˙}{-} y)) = (y \in Y ⟼ N (A \underset{˙}{-} y))$
79		breq2	$⊢ w = N (A \underset{˙}{-} y) \to (\sqrt{S^{2} + r} \leq w \leftrightarrow \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y))$
80	78 79	ralrnmptw	$⊢ \forall y \in Y N (A \underset{˙}{-} y) \in V \to (\forall w \in ran (y \in Y ⟼ N (A \underset{˙}{-} y)) \sqrt{S^{2} + r} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y))$
81	77 80	ax-mp	$⊢ \forall w \in ran (y \in Y ⟼ N (A \underset{˙}{-} y)) \sqrt{S^{2} + r} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y)$
82	75 81	bitri	$⊢ \forall w \in R \sqrt{S^{2} + r} \leq w \leftrightarrow \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y)$
83	74 82	bitrdi	$⊢ (φ \land r \in ℝ^{+}) \to (\sqrt{S^{2} + r} \leq sup (R ℝ <) \leftrightarrow \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y))$
84	72 83	bitrid	$⊢ (φ \land r \in ℝ^{+}) \to (\sqrt{S^{2} + r} \leq S \leftrightarrow \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y))$
85	71 84	mtbid	$⊢ (φ \land r \in ℝ^{+}) \to \neg \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y)$
86		rexnal	$⊢ \exists y \in Y \neg \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y) \leftrightarrow \neg \forall y \in Y \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y)$
87	85 86	sylibr	$⊢ (φ \land r \in ℝ^{+}) \to \exists y \in Y \neg \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y)$
88	61	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to \sqrt{S^{2} + r} \in ℝ$
89		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
90	4 89	syl	$⊢ φ \to U \in NrmGrp$
91		ngpms	$⊢ U \in NrmGrp \to U \in MetSp$
92	1 11	msmet	$⊢ U \in MetSp \to D \in Met (X)$
93	90 91 92	3syl	$⊢ φ \to D \in Met (X)$
94	93	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to D \in Met (X)$
95	7	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A \in X$
96		eqid	$⊢ LSubSp (U) = LSubSp (U)$
97	1 96	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
98	14 97	syl	$⊢ (φ \land r \in ℝ^{+}) \to Y \subseteq X$
99	98	sselda	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to y \in X$
100		metcl	$⊢ (D \in Met (X) \land A \in X \land y \in X) \to A D y \in ℝ$
101	94 95 99 100	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A D y \in ℝ$
102	67	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to 0 \leq \sqrt{S^{2} + r}$
103		metge0	$⊢ (D \in Met (X) \land A \in X \land y \in X) \to 0 \leq A D y$
104	94 95 99 103	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to 0 \leq A D y$
105	88 101 102 104	le2sqd	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\sqrt{S^{2} + r} \leq A D y \leftrightarrow {\sqrt{S^{2} + r}}^{2} \leq {(A D y)}^{2})$
106	11	oveqi	$⊢ A D y = A ({dist (U) ↾}_{(X \times X)}) y$
107	95 99	ovresd	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A ({dist (U) ↾}_{(X \times X)}) y = A dist (U) y$
108	106 107	eqtrid	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A D y = A dist (U) y$
109	90	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to U \in NrmGrp$
110		eqid	$⊢ dist (U) = dist (U)$
111	3 1 2 110	ngpds	$⊢ (U \in NrmGrp \land A \in X \land y \in X) \to A dist (U) y = N (A \underset{˙}{-} y)$
112	109 95 99 111	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A dist (U) y = N (A \underset{˙}{-} y)$
113	108 112	eqtrd	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to A D y = N (A \underset{˙}{-} y)$
114	113	breq2d	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\sqrt{S^{2} + r} \leq A D y \leftrightarrow \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y))$
115	40	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to {\sqrt{S^{2} + r}}^{2} = S^{2} + r$
116	115	breq1d	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to ({\sqrt{S^{2} + r}}^{2} \leq {(A D y)}^{2} \leftrightarrow S^{2} + r \leq {(A D y)}^{2})$
117	105 114 116	3bitr3d	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y) \leftrightarrow S^{2} + r \leq {(A D y)}^{2})$
118	117	notbid	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\neg \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y) \leftrightarrow \neg S^{2} + r \leq {(A D y)}^{2})$
119	38	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to S^{2} + r \in ℝ$
120	101	resqcld	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to {(A D y)}^{2} \in ℝ$
121	119 120	letrid	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (S^{2} + r \leq {(A D y)}^{2} \lor {(A D y)}^{2} \leq S^{2} + r)$
122	121	ord	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\neg S^{2} + r \leq {(A D y)}^{2} \to {(A D y)}^{2} \leq S^{2} + r)$
123	118 122	sylbid	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to (\neg \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y) \to {(A D y)}^{2} \leq S^{2} + r)$
124	123	reximdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists y \in Y \neg \sqrt{S^{2} + r} \leq N (A \underset{˙}{-} y) \to \exists y \in Y {(A D y)}^{2} \leq S^{2} + r)$
125	87 124	mpd	$⊢ (φ \land r \in ℝ^{+}) \to \exists y \in Y {(A D y)}^{2} \leq S^{2} + r$
126		rabn0	$⊢ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \neq \emptyset \leftrightarrow \exists y \in Y {(A D y)}^{2} \leq S^{2} + r$
127	125 126	sylibr	$⊢ (φ \land r \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\} \neq \emptyset$
128	127	necomd	$⊢ (φ \land r \in ℝ^{+}) \to \emptyset \neq \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
129	128	neneqd	$⊢ (φ \land r \in ℝ^{+}) \to \neg \emptyset = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
130	129	nrexdv	$⊢ φ \to \neg \exists r \in ℝ^{+} \emptyset = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
131	12	eleq2i	$⊢ \emptyset \in F \leftrightarrow \emptyset \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
132		0ex	$⊢ \emptyset \in V$
133	22	elrnmpt	$⊢ \emptyset \in V \to (\emptyset \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) \leftrightarrow \exists r \in ℝ^{+} \emptyset = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
134	132 133	ax-mp	$⊢ \emptyset \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}) \leftrightarrow \exists r \in ℝ^{+} \emptyset = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
135	131 134	bitri	$⊢ \emptyset \in F \leftrightarrow \exists r \in ℝ^{+} \emptyset = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
136	130 135	sylnibr	$⊢ φ \to \neg \emptyset \in F$
137		df-nel	$⊢ \emptyset \notin F \leftrightarrow \neg \emptyset \in F$
138	136 137	sylibr	$⊢ φ \to \emptyset \notin F$
139	56	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to S \in ℝ$
140	139	resqcld	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to S^{2} \in ℝ$
141	37	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to r \in ℝ$
142	120 140 141	lesubadd2d	$⊢ ((φ \land r \in ℝ^{+}) \land y \in Y) \to ({(A D y)}^{2} - S^{2} \leq r \leftrightarrow {(A D y)}^{2} \leq S^{2} + r)$
143	142	rabbidva	$⊢ (φ \land r \in ℝ^{+}) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\} = \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\}$
144	143	mpteq2dva	$⊢ φ \to (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) = (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
145	144	rneqd	$⊢ φ \to ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} \leq S^{2} + r\})$
146	12 145	eqtr4id	$⊢ φ \to F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\})$
147	146	eleq2d	$⊢ φ \to (u \in F \leftrightarrow u \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}))$
148		breq2	$⊢ r = s \to ({(A D y)}^{2} - S^{2} \leq r \leftrightarrow {(A D y)}^{2} - S^{2} \leq s)$
149	148	rabbidv	$⊢ r = s \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\} = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\}$
150	149	cbvmptv	$⊢ (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) = (s \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\})$
151	150	elrnmpt	$⊢ u \in V \to (u \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) \leftrightarrow \exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\})$
152	151	elv	$⊢ u \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) \leftrightarrow \exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\}$
153	147 152	bitrdi	$⊢ φ \to (u \in F \leftrightarrow \exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\})$
154	146	eleq2d	$⊢ φ \to (v \in F \leftrightarrow v \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}))$
155		breq2	$⊢ r = t \to ({(A D y)}^{2} - S^{2} \leq r \leftrightarrow {(A D y)}^{2} - S^{2} \leq t)$
156	155	rabbidv	$⊢ r = t \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\} = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}$
157	156	cbvmptv	$⊢ (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) = (t \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\})$
158	157	elrnmpt	$⊢ v \in V \to (v \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) \leftrightarrow \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\})$
159	158	elv	$⊢ v \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) \leftrightarrow \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}$
160	154 159	bitrdi	$⊢ φ \to (v \in F \leftrightarrow \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\})$
161	153 160	anbi12d	$⊢ φ \to ((u \in F \land v \in F) \leftrightarrow (\exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}))$
162		reeanv	$⊢ \exists s \in ℝ^{+} \exists t \in ℝ^{+} (u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \leftrightarrow (\exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\})$
163	93	ad2antrr	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to D \in Met (X)$
164	7	ad2antrr	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to A \in X$
165	5 97	syl	$⊢ φ \to Y \subseteq X$
166	165	adantr	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to Y \subseteq X$
167	166	sselda	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to y \in X$
168	163 164 167 100	syl3anc	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to A D y \in ℝ$
169	168	resqcld	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to {(A D y)}^{2} \in ℝ$
170	32	ad2antrr	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to S^{2} \in ℝ$
171	169 170	resubcld	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to {(A D y)}^{2} - S^{2} \in ℝ$
172		simplrl	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to s \in ℝ^{+}$
173	172	rpred	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to s \in ℝ$
174		simplrr	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to t \in ℝ^{+}$
175	174	rpred	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to t \in ℝ$
176		lemin	$⊢ ({(A D y)}^{2} - S^{2} \in ℝ \land s \in ℝ \land t \in ℝ) \to ({(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t) \leftrightarrow ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t))$
177	171 173 175 176	syl3anc	$⊢ ((φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \land y \in Y) \to ({(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t) \leftrightarrow ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t))$
178	177	rabbidva	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} = \{y \in Y \| ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t)\}$
179		ifcl	$⊢ (s \in ℝ^{+} \land t \in ℝ^{+}) \to if (s \leq t, s, t) \in ℝ^{+}$
180	5	adantr	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to Y \in LSubSp (U)$
181		rabexg	$⊢ Y \in LSubSp (U) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in V$
182	180 181	syl	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in V$
183		eqid	$⊢ (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\}) = (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\})$
184		breq2	$⊢ r = if (s \leq t, s, t) \to ({(A D y)}^{2} - S^{2} \leq r \leftrightarrow {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t))$
185	184	rabbidv	$⊢ r = if (s \leq t, s, t) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\} = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\}$
186	183 185	elrnmpt1s	$⊢ (if (s \leq t, s, t) \in ℝ^{+} \land \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in V) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\})$
187	179 182 186	syl2an2	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\})$
188	146	adantr	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to F = ran (r \in ℝ^{+} ⟼ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq r\})$
189	187 188	eleqtrrd	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to \{y \in Y \| {(A D y)}^{2} - S^{2} \leq if (s \leq t, s, t)\} \in F$
190	178 189	eqeltrrd	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to \{y \in Y \| ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t)\} \in F$
191		ineq12	$⊢ (u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to u \cap v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \cap \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}$
192		inrab	$⊢ \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \cap \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\} = \{y \in Y \| ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t)\}$
193	191 192	eqtrdi	$⊢ (u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to u \cap v = \{y \in Y \| ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t)\}$
194	193	eleq1d	$⊢ (u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to (u \cap v \in F \leftrightarrow \{y \in Y \| ({(A D y)}^{2} - S^{2} \leq s \land {(A D y)}^{2} - S^{2} \leq t)\} \in F)$
195	190 194	syl5ibrcom	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to ((u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to u \cap v \in F)$
196		vex	$⊢ u \in V$
197	196	inex1	$⊢ u \cap v \in V$
198	197	pwid	$⊢ u \cap v \in 𝒫 (u \cap v)$
199		inelcm	$⊢ (u \cap v \in F \land u \cap v \in 𝒫 (u \cap v)) \to F \cap 𝒫 (u \cap v) \neq \emptyset$
200	198 199	mpan2	$⊢ u \cap v \in F \to F \cap 𝒫 (u \cap v) \neq \emptyset$
201	195 200	syl6	$⊢ (φ \land (s \in ℝ^{+} \land t \in ℝ^{+})) \to ((u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to F \cap 𝒫 (u \cap v) \neq \emptyset)$
202	201	rexlimdvva	$⊢ φ \to (\exists s \in ℝ^{+} \exists t \in ℝ^{+} (u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to F \cap 𝒫 (u \cap v) \neq \emptyset)$
203	162 202	biimtrrid	$⊢ φ \to ((\exists s \in ℝ^{+} u = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq s\} \land \exists t \in ℝ^{+} v = \{y \in Y \| {(A D y)}^{2} - S^{2} \leq t\}) \to F \cap 𝒫 (u \cap v) \neq \emptyset)$
204	161 203	sylbid	$⊢ φ \to ((u \in F \land v \in F) \to F \cap 𝒫 (u \cap v) \neq \emptyset)$
205	204	ralrimivv	$⊢ φ \to \forall u \in F \forall v \in F F \cap 𝒫 (u \cap v) \neq \emptyset$
206	30 138 205	3jca	$⊢ φ \to (F \neq \emptyset \land \emptyset \notin F \land \forall u \in F \forall v \in F F \cap 𝒫 (u \cap v) \neq \emptyset)$
207		isfbas	$⊢ Y \in LSubSp (U) \to (F \in fBas (Y) \leftrightarrow (F \subseteq 𝒫 Y \land (F \neq \emptyset \land \emptyset \notin F \land \forall u \in F \forall v \in F F \cap 𝒫 (u \cap v) \neq \emptyset)))$
208	5 207	syl	$⊢ φ \to (F \in fBas (Y) \leftrightarrow (F \subseteq 𝒫 Y \land (F \neq \emptyset \land \emptyset \notin F \land \forall u \in F \forall v \in F F \cap 𝒫 (u \cap v) \neq \emptyset)))$
209	20 206 208	mpbir2and	$⊢ φ \to F \in fBas (Y)$

Metamath Proof Explorer

Theorem minveclem3b

Proof