minvecolem7

Description: Lemma for minveco . Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-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))$
	minveco.s	$⊢ S = sup (R ℝ <)$
Assertion	minvecolem7	$⊢ φ \to \exists! x \in Y \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 = sup (R ℝ <)$
12	1 2 3 4 5 6 7 8 9 10 11	minvecolem5	$⊢ φ \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$
13	5	ad2antrr	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to U \in {CPreHil}_{OLD}$
14	6	ad2antrr	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to W \in (SubSp (U) \cap CBan)$
15	7	ad2antrr	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to A \in X$
16		0re	$⊢ 0 \in ℝ$
17	16	a1i	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to 0 \in ℝ$
18		0le0	$⊢ 0 \leq 0$
19	18	a1i	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to 0 \leq 0$
20		simplrl	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to x \in Y$
21		simplrr	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to w \in Y$
22		simprl	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to {(A D x)}^{2} \leq S^{2} + 0$
23		simprr	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to {(A D w)}^{2} \leq S^{2} + 0$
24	1 2 3 4 13 14 15 8 9 10 11 17 19 20 21 22 23	minvecolem2	$⊢ ((φ \land (x \in Y \land w \in Y)) \land ({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0)) \to {(x D w)}^{2} \leq 4 \cdot 0$
25	24	ex	$⊢ (φ \land (x \in Y \land w \in Y)) \to (({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0) \to {(x D w)}^{2} \leq 4 \cdot 0)$
26	1 2 3 4 5 6 7 8 9 10 11	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))$
27	26	adantrr	$⊢ (φ \land (x \in Y \land w \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))$
28	1 2 3 4 5 6 7 8 9 10 11	minvecolem6	$⊢ (φ \land w \in Y) \to ({(A D w)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A M w) \leq N (A M y))$
29	28	adantrl	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(A D w)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A M w) \leq N (A M y))$
30	27 29	anbi12d	$⊢ (φ \land (x \in Y \land w \in Y)) \to (({(A D x)}^{2} \leq S^{2} + 0 \land {(A D w)}^{2} \leq S^{2} + 0) \leftrightarrow (\forall y \in Y N (A M x) \leq N (A M y) \land \forall y \in Y N (A M w) \leq N (A M y)))$
31		4cn	$⊢ 4 \in ℂ$
32	31	mul01i	$⊢ 4 \cdot 0 = 0$
33	32	breq2i	$⊢ {(x D w)}^{2} \leq 4 \cdot 0 \leftrightarrow {(x D w)}^{2} \leq 0$
34		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
35	5 34	syl	$⊢ φ \to U \in NrmCVec$
36	35	adantr	$⊢ (φ \land (x \in Y \land w \in Y)) \to U \in NrmCVec$
37	1 8	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
38	36 37	syl	$⊢ (φ \land (x \in Y \land w \in Y)) \to D \in Met (X)$
39		inss1	$⊢ SubSp (U) \cap CBan \subseteq SubSp (U)$
40	39 6	sselid	$⊢ φ \to W \in SubSp (U)$
41		eqid	$⊢ SubSp (U) = SubSp (U)$
42	1 4 41	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
43	35 40 42	syl2anc	$⊢ φ \to Y \subseteq X$
44	43	adantr	$⊢ (φ \land (x \in Y \land w \in Y)) \to Y \subseteq X$
45		simprl	$⊢ (φ \land (x \in Y \land w \in Y)) \to x \in Y$
46	44 45	sseldd	$⊢ (φ \land (x \in Y \land w \in Y)) \to x \in X$
47		simprr	$⊢ (φ \land (x \in Y \land w \in Y)) \to w \in Y$
48	44 47	sseldd	$⊢ (φ \land (x \in Y \land w \in Y)) \to w \in X$
49		metcl	$⊢ (D \in Met (X) \land x \in X \land w \in X) \to x D w \in ℝ$
50	38 46 48 49	syl3anc	$⊢ (φ \land (x \in Y \land w \in Y)) \to x D w \in ℝ$
51	50	sqge0d	$⊢ (φ \land (x \in Y \land w \in Y)) \to 0 \leq {(x D w)}^{2}$
52	51	biantrud	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} \leq 0 \leftrightarrow ({(x D w)}^{2} \leq 0 \land 0 \leq {(x D w)}^{2}))$
53	50	resqcld	$⊢ (φ \land (x \in Y \land w \in Y)) \to {(x D w)}^{2} \in ℝ$
54		letri3	$⊢ ({(x D w)}^{2} \in ℝ \land 0 \in ℝ) \to ({(x D w)}^{2} = 0 \leftrightarrow ({(x D w)}^{2} \leq 0 \land 0 \leq {(x D w)}^{2}))$
55	53 16 54	sylancl	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} = 0 \leftrightarrow ({(x D w)}^{2} \leq 0 \land 0 \leq {(x D w)}^{2}))$
56	50	recnd	$⊢ (φ \land (x \in Y \land w \in Y)) \to x D w \in ℂ$
57		sqeq0	$⊢ x D w \in ℂ \to ({(x D w)}^{2} = 0 \leftrightarrow x D w = 0)$
58	56 57	syl	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} = 0 \leftrightarrow x D w = 0)$
59		meteq0	$⊢ (D \in Met (X) \land x \in X \land w \in X) \to (x D w = 0 \leftrightarrow x = w)$
60	38 46 48 59	syl3anc	$⊢ (φ \land (x \in Y \land w \in Y)) \to (x D w = 0 \leftrightarrow x = w)$
61	58 60	bitrd	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} = 0 \leftrightarrow x = w)$
62	52 55 61	3bitr2d	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} \leq 0 \leftrightarrow x = w)$
63	33 62	syl5bb	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} \leq 4 \cdot 0 \leftrightarrow x = w)$
64	25 30 63	3imtr3d	$⊢ (φ \land (x \in Y \land w \in Y)) \to ((\forall y \in Y N (A M x) \leq N (A M y) \land \forall y \in Y N (A M w) \leq N (A M y)) \to x = w)$
65	64	ralrimivva	$⊢ φ \to \forall x \in Y \forall w \in Y ((\forall y \in Y N (A M x) \leq N (A M y) \land \forall y \in Y N (A M w) \leq N (A M y)) \to x = w)$
66		oveq2	$⊢ x = w \to A M x = A M w$
67	66	fveq2d	$⊢ x = w \to N (A M x) = N (A M w)$
68	67	breq1d	$⊢ x = w \to (N (A M x) \leq N (A M y) \leftrightarrow N (A M w) \leq N (A M y))$
69	68	ralbidv	$⊢ x = w \to (\forall y \in Y N (A M x) \leq N (A M y) \leftrightarrow \forall y \in Y N (A M w) \leq N (A M y))$
70	69	reu4	$⊢ \exists! x \in Y \forall y \in Y N (A M x) \leq N (A M y) \leftrightarrow (\exists x \in Y \forall y \in Y N (A M x) \leq N (A M y) \land \forall x \in Y \forall w \in Y ((\forall y \in Y N (A M x) \leq N (A M y) \land \forall y \in Y N (A M w) \leq N (A M y)) \to x = w))$
71	12 65 70	sylanbrc	$⊢ φ \to \exists! x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

Metamath Proof Explorer

Theorem minvecolem7

Proof