minveclem7

Description: Lemma for minvec . Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-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)}$
Assertion	minveclem7	$⊢ φ \to \exists! x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} 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	1 2 3 4 5 6 7 8 9 10 11	minveclem5	$⊢ φ \to \exists x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
13	4	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$
14	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 Y \in LSubSp (U)$
15	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 U ↾_{𝑠} Y \in CMetSp$
16	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$
17		0re	$⊢ 0 \in ℝ$
18	17	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 ℝ$
19		0le0	$⊢ 0 \leq 0$
20	19	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$
21		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$
22		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$
23		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$
24		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$
25	1 2 3 13 14 15 16 8 9 10 11 18 20 21 22 23 24	minveclem2	$⊢ ((φ \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$
26	25	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)$
27	1 2 3 4 5 6 7 8 9 10 11	minveclem6	$⊢ (φ \land x \in Y) \to ({(A D x)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))$
28	27	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 \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))$
29	1 2 3 4 5 6 7 8 9 10 11	minveclem6	$⊢ (φ \land w \in Y) \to ({(A D w)}^{2} \leq S^{2} + 0 \leftrightarrow \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y))$
30	29	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 \underset{˙}{-} w) \leq N (A \underset{˙}{-} y))$
31	28 30	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 \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \land \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y)))$
32		4cn	$⊢ 4 \in ℂ$
33	32	mul01i	$⊢ 4 \cdot 0 = 0$
34	33	breq2i	$⊢ {(x D w)}^{2} \leq 4 \cdot 0 \leftrightarrow {(x D w)}^{2} \leq 0$
35		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
36		ngpms	$⊢ U \in NrmGrp \to U \in MetSp$
37	4 35 36	3syl	$⊢ φ \to U \in MetSp$
38	37	adantr	$⊢ (φ \land (x \in Y \land w \in Y)) \to U \in MetSp$
39	1 11	msmet	$⊢ U \in MetSp \to D \in Met (X)$
40	38 39	syl	$⊢ (φ \land (x \in Y \land w \in Y)) \to D \in Met (X)$
41		eqid	$⊢ LSubSp (U) = LSubSp (U)$
42	1 41	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
43	5 42	syl	$⊢ φ \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	40 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 17 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	40 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	34 62	bitrid	$⊢ (φ \land (x \in Y \land w \in Y)) \to ({(x D w)}^{2} \leq 4 \cdot 0 \leftrightarrow x = w)$
64	26 31 63	3imtr3d	$⊢ (φ \land (x \in Y \land w \in Y)) \to ((\forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \land \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y)) \to x = w)$
65	64	ralrimivva	$⊢ φ \to \forall x \in Y \forall w \in Y ((\forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \land \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y)) \to x = w)$
66		oveq2	$⊢ x = w \to A \underset{˙}{-} x = A \underset{˙}{-} w$
67	66	fveq2d	$⊢ x = w \to N (A \underset{˙}{-} x) = N (A \underset{˙}{-} w)$
68	67	breq1d	$⊢ x = w \to (N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y))$
69	68	ralbidv	$⊢ x = w \to (\forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y))$
70	69	reu4	$⊢ \exists! x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow (\exists x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \land \forall x \in Y \forall w \in Y ((\forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \land \forall y \in Y N (A \underset{˙}{-} w) \leq N (A \underset{˙}{-} y)) \to x = w))$
71	12 65 70	sylanbrc	$⊢ φ \to \exists! x \in Y \forall y \in Y N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$

Metamath Proof Explorer

Theorem minveclem7

Proof