minvecolem6

Description: Lemma for minveco . Any minimal point is less than S away from A . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (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))$
	minveco.s	$⊢ S = inf (R ℝ <)$
Assertion	minvecolem6	$⊢ (φ \land x \in Y) \to ({(A D x)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A M x) \leq N (A M y))$

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		minveco.s	$⊢ S = inf (R ℝ <)$
12		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
13	5 12	syl	$⊢ φ \to U \in NrmCVec$
14	13	adantr	$⊢ (φ \land x \in Y) \to U \in NrmCVec$
15	7	adantr	$⊢ (φ \land x \in Y) \to A \in X$
16		inss1	$⊢ SubSp (U) \cap CBan \subseteq SubSp (U)$
17	16 6	sselid	$⊢ φ \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	13 17 19	syl2anc	$⊢ φ \to Y \subseteq X$
21	20	sselda	$⊢ (φ \land x \in Y) \to x \in X$
22	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land A \in X \land x \in X) \to A D x = N (A M x)$
23	14 15 21 22	syl3anc	$⊢ (φ \land x \in Y) \to A D x = N (A M x)$
24	23	oveq1d	$⊢ (φ \land x \in Y) \to {(A D x)}^{2} = {N (A M x)}^{2}$
25	1 2 3 4 5 6 7 8 9 10	minvecolem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
26	25	adantr	$⊢ (φ \land x \in Y) \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
27	26	simp1d	$⊢ (φ \land x \in Y) \to R \subseteq ℝ$
28	26	simp2d	$⊢ (φ \land x \in Y) \to R \neq \emptyset$
29		0red	$⊢ (φ \land x \in Y) \to 0 \in ℝ$
30	26	simp3d	$⊢ (φ \land x \in Y) \to \forall w \in R 0 \leq w$
31		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
32	31	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
33	32	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
34	29 30 33	syl2anc	$⊢ (φ \land x \in Y) \to \exists x \in ℝ \forall w \in R x \leq w$
35		infrecl	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \to inf (R ℝ <) \in ℝ$
36	27 28 34 35	syl3anc	$⊢ (φ \land x \in Y) \to inf (R ℝ <) \in ℝ$
37	11 36	eqeltrid	$⊢ (φ \land x \in Y) \to S \in ℝ$
38	37	resqcld	$⊢ (φ \land x \in Y) \to S^{2} \in ℝ$
39	38	recnd	$⊢ (φ \land x \in Y) \to S^{2} \in ℂ$
40	39	addridd	$⊢ (φ \land x \in Y) \to S^{2} + 0 = S^{2}$
41	24 40	breq12d	$⊢ (φ \land x \in Y) \to ({(A D x)}^{2} \leq S^{2} + 0 \leftrightarrow {N (A M x)}^{2} \leq S^{2})$
42	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land x \in X) \to A M x \in X$
43	14 15 21 42	syl3anc	$⊢ (φ \land x \in Y) \to A M x \in X$
44	1 3	nvcl	$⊢ (U \in NrmCVec \land A M x \in X) \to N (A M x) \in ℝ$
45	14 43 44	syl2anc	$⊢ (φ \land x \in Y) \to N (A M x) \in ℝ$
46	1 3	nvge0	$⊢ (U \in NrmCVec \land A M x \in X) \to 0 \leq N (A M x)$
47	14 43 46	syl2anc	$⊢ (φ \land x \in Y) \to 0 \leq N (A M x)$
48		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land 0 \in ℝ) \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
49	27 28 34 29 48	syl31anc	$⊢ (φ \land x \in Y) \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
50	30 49	mpbird	$⊢ (φ \land x \in Y) \to 0 \leq inf (R ℝ <)$
51	50 11	breqtrrdi	$⊢ (φ \land x \in Y) \to 0 \leq S$
52	45 37 47 51	le2sqd	$⊢ (φ \land x \in Y) \to (N (A M x) \leq S \leftrightarrow {N (A M x)}^{2} \leq S^{2})$
53	11	breq2i	$⊢ N (A M x) \leq S \leftrightarrow N (A M x) \leq inf (R ℝ <)$
54		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land N (A M x) \in ℝ) \to (N (A M x) \leq inf (R ℝ <) \leftrightarrow \forall w \in R N (A M x) \leq w)$
55	27 28 34 45 54	syl31anc	$⊢ (φ \land x \in Y) \to (N (A M x) \leq inf (R ℝ <) \leftrightarrow \forall w \in R N (A M x) \leq w)$
56	53 55	bitrid	$⊢ (φ \land x \in Y) \to (N (A M x) \leq S \leftrightarrow \forall w \in R N (A M x) \leq w)$
57	41 52 56	3bitr2d	$⊢ (φ \land x \in Y) \to ({(A D x)}^{2} \leq S^{2} + 0 \leftrightarrow \forall w \in R N (A M x) \leq w)$
58	10	raleqi	$⊢ \forall w \in R N (A M x) \leq w \leftrightarrow \forall w \in ran (y \in Y ⟼ N (A M y)) N (A M x) \leq w$
59		fvex	$⊢ N (A M y) \in V$
60	59	rgenw	$⊢ \forall y \in Y N (A M y) \in V$
61		eqid	$⊢ (y \in Y ⟼ N (A M y)) = (y \in Y ⟼ N (A M y))$
62		breq2	$⊢ w = N (A M y) \to (N (A M x) \leq w \leftrightarrow N (A M x) \leq N (A M y))$
63	61 62	ralrnmptw	$⊢ \forall y \in Y N (A M y) \in V \to (\forall w \in ran (y \in Y ⟼ N (A M y)) N (A M x) \leq w \leftrightarrow \forall y \in Y N (A M x) \leq N (A M y))$
64	60 63	ax-mp	$⊢ \forall w \in ran (y \in Y ⟼ N (A M y)) N (A M x) \leq w \leftrightarrow \forall y \in Y N (A M x) \leq N (A M y)$
65	58 64	bitri	$⊢ \forall w \in R N (A M x) \leq w \leftrightarrow \forall y \in Y N (A M x) \leq N (A M y)$
66	57 65	bitrdi	$⊢ (φ \land x \in Y) \to ({(A D x)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A M x) \leq N (A M y))$

Metamath Proof Explorer

Theorem minvecolem6

Proof