minvecolem1

Description: Lemma for minveco . The set of all distances from points of Y to A are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	$⊢ X = BaseSet (U)$
	minveco.m	$⊢ M = -_{v} (U)$
	minveco.n	$⊢ N = {norm}_{CV} (U)$
	minveco.y	$⊢ Y = BaseSet (W)$
	minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
	minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
	minveco.a	$⊢ φ \to A \in X$
	minveco.d	$⊢ D = IndMet (U)$
	minveco.j	$⊢ J = MetOpen (D)$
	minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
Assertion	minvecolem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$

Proof

Step	Hyp	Ref	Expression
1		minveco.x	$⊢ X = BaseSet (U)$
2		minveco.m	$⊢ M = -_{v} (U)$
3		minveco.n	$⊢ N = {norm}_{CV} (U)$
4		minveco.y	$⊢ Y = BaseSet (W)$
5		minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
6		minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
7		minveco.a	$⊢ φ \to A \in X$
8		minveco.d	$⊢ D = IndMet (U)$
9		minveco.j	$⊢ J = MetOpen (D)$
10		minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
11		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
12	5 11	syl	$⊢ φ \to U \in NrmCVec$
13	12	adantr	$⊢ (φ \land y \in Y) \to U \in NrmCVec$
14	7	adantr	$⊢ (φ \land y \in Y) \to A \in X$
15		elin	$⊢ W \in (SubSp (U) \cap CBan) \leftrightarrow (W \in SubSp (U) \land W \in CBan)$
16	6 15	sylib	$⊢ φ \to (W \in SubSp (U) \land W \in CBan)$
17	16	simpld	$⊢ φ \to W \in SubSp (U)$
18		eqid	$⊢ SubSp (U) = SubSp (U)$
19	1 4 18	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
20	12 17 19	syl2anc	$⊢ φ \to Y \subseteq X$
21	20	sselda	$⊢ (φ \land y \in Y) \to y \in X$
22	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land y \in X) \to A M y \in X$
23	13 14 21 22	syl3anc	$⊢ (φ \land y \in Y) \to A M y \in X$
24	1 3	nvcl	$⊢ (U \in NrmCVec \land A M y \in X) \to N (A M y) \in ℝ$
25	13 23 24	syl2anc	$⊢ (φ \land y \in Y) \to N (A M y) \in ℝ$
26	25	fmpttd	$⊢ φ \to (y \in Y ⟼ N (A M y)) : Y ⟶ ℝ$
27	26	frnd	$⊢ φ \to ran (y \in Y ⟼ N (A M y)) \subseteq ℝ$
28	10 27	eqsstrid	$⊢ φ \to R \subseteq ℝ$
29	16	simprd	$⊢ φ \to W \in CBan$
30		bnnv	$⊢ W \in CBan \to W \in NrmCVec$
31		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
32	4 31	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in Y$
33	29 30 32	3syl	$⊢ φ \to 0_{vec} (W) \in Y$
34		fvex	$⊢ N (A M y) \in V$
35		eqid	$⊢ (y \in Y ⟼ N (A M y)) = (y \in Y ⟼ N (A M y))$
36	34 35	dmmpti	$⊢ dom (y \in Y ⟼ N (A M y)) = Y$
37	33 36	eleqtrrdi	$⊢ φ \to 0_{vec} (W) \in dom (y \in Y ⟼ N (A M y))$
38	37	ne0d	$⊢ φ \to dom (y \in Y ⟼ N (A M y)) \neq \emptyset$
39		dm0rn0	$⊢ dom (y \in Y ⟼ N (A M y)) = \emptyset \leftrightarrow ran (y \in Y ⟼ N (A M y)) = \emptyset$
40	10	eqeq1i	$⊢ R = \emptyset \leftrightarrow ran (y \in Y ⟼ N (A M y)) = \emptyset$
41	39 40	bitr4i	$⊢ dom (y \in Y ⟼ N (A M y)) = \emptyset \leftrightarrow R = \emptyset$
42	41	necon3bii	$⊢ dom (y \in Y ⟼ N (A M y)) \neq \emptyset \leftrightarrow R \neq \emptyset$
43	38 42	sylib	$⊢ φ \to R \neq \emptyset$
44	1 3	nvge0	$⊢ (U \in NrmCVec \land A M y \in X) \to 0 \leq N (A M y)$
45	13 23 44	syl2anc	$⊢ (φ \land y \in Y) \to 0 \leq N (A M y)$
46	45	ralrimiva	$⊢ φ \to \forall y \in Y 0 \leq N (A M y)$
47	34	rgenw	$⊢ \forall y \in Y N (A M y) \in V$
48		breq2	$⊢ w = N (A M y) \to (0 \leq w \leftrightarrow 0 \leq N (A M y))$
49	35 48	ralrnmptw	$⊢ \forall y \in Y N (A M y) \in V \to (\forall w \in ran (y \in Y ⟼ N (A M y)) 0 \leq w \leftrightarrow \forall y \in Y 0 \leq N (A M y))$
50	47 49	ax-mp	$⊢ \forall w \in ran (y \in Y ⟼ N (A M y)) 0 \leq w \leftrightarrow \forall y \in Y 0 \leq N (A M y)$
51	46 50	sylibr	$⊢ φ \to \forall w \in ran (y \in Y ⟼ N (A M y)) 0 \leq w$
52	10	raleqi	$⊢ \forall w \in R 0 \leq w \leftrightarrow \forall w \in ran (y \in Y ⟼ N (A M y)) 0 \leq w$
53	51 52	sylibr	$⊢ φ \to \forall w \in R 0 \leq w$
54	28 43 53	3jca	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$

Metamath Proof Explorer

Theorem minvecolem1

Proof