minvecolem2

Description: Lemma for minveco . Any two points K and L in Y are close to each other if they are close to the infimum of distance to 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 ℝ <)$
	minvecolem2.1	$⊢ φ \to B \in ℝ$
	minvecolem2.2	$⊢ φ \to 0 \leq B$
	minvecolem2.3	$⊢ φ \to K \in Y$
	minvecolem2.4	$⊢ φ \to L \in Y$
	minvecolem2.5	$⊢ φ \to {(A D K)}^{2} \leq S^{2} + B$
	minvecolem2.6	$⊢ φ \to {(A D L)}^{2} \leq S^{2} + B$
Assertion	minvecolem2	$⊢ φ \to {(K D L)}^{2} \leq 4 B$

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		minvecolem2.1	$⊢ φ \to B \in ℝ$
13		minvecolem2.2	$⊢ φ \to 0 \leq B$
14		minvecolem2.3	$⊢ φ \to K \in Y$
15		minvecolem2.4	$⊢ φ \to L \in Y$
16		minvecolem2.5	$⊢ φ \to {(A D K)}^{2} \leq S^{2} + B$
17		minvecolem2.6	$⊢ φ \to {(A D L)}^{2} \leq S^{2} + B$
18		4re	$⊢ 4 \in ℝ$
19	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)$
20	19	simp1d	$⊢ φ \to R \subseteq ℝ$
21	19	simp2d	$⊢ φ \to R \neq \emptyset$
22		0re	$⊢ 0 \in ℝ$
23	19	simp3d	$⊢ φ \to \forall w \in R 0 \leq w$
24		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
25	24	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
26	25	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
27	22 23 26	sylancr	$⊢ φ \to \exists x \in ℝ \forall w \in R x \leq w$
28		infrecl	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \to inf (R ℝ <) \in ℝ$
29	20 21 27 28	syl3anc	$⊢ φ \to inf (R ℝ <) \in ℝ$
30	11 29	eqeltrid	$⊢ φ \to S \in ℝ$
31	30	resqcld	$⊢ φ \to S^{2} \in ℝ$
32		remulcl	$⊢ (4 \in ℝ \land S^{2} \in ℝ) \to 4 S^{2} \in ℝ$
33	18 31 32	sylancr	$⊢ φ \to 4 S^{2} \in ℝ$
34		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
35	5 34	syl	$⊢ φ \to U \in NrmCVec$
36	1 8	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
37	35 36	syl	$⊢ φ \to D \in Met (X)$
38		inss1	$⊢ SubSp (U) \cap CBan \subseteq SubSp (U)$
39	38 6	sselid	$⊢ φ \to W \in SubSp (U)$
40		eqid	$⊢ SubSp (U) = SubSp (U)$
41	1 4 40	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
42	35 39 41	syl2anc	$⊢ φ \to Y \subseteq X$
43	42 14	sseldd	$⊢ φ \to K \in X$
44	42 15	sseldd	$⊢ φ \to L \in X$
45		metcl	$⊢ (D \in Met (X) \land K \in X \land L \in X) \to K D L \in ℝ$
46	37 43 44 45	syl3anc	$⊢ φ \to K D L \in ℝ$
47	46	resqcld	$⊢ φ \to {(K D L)}^{2} \in ℝ$
48	33 47	readdcld	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \in ℝ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		halfcl	$⊢ 1 \in ℂ \to \frac{1}{2} \in ℂ$
51	49 50	mp1i	$⊢ φ \to \frac{1}{2} \in ℂ$
52		eqid	$⊢ +_{v} (U) = +_{v} (U)$
53		eqid	$⊢ +_{v} (W) = +_{v} (W)$
54	4 52 53 40	sspgval	$⊢ ((U \in NrmCVec \land W \in SubSp (U)) \land (K \in Y \land L \in Y)) \to K +_{v} (W) L = K +_{v} (U) L$
55	35 39 14 15 54	syl22anc	$⊢ φ \to K +_{v} (W) L = K +_{v} (U) L$
56	40	sspnv	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to W \in NrmCVec$
57	35 39 56	syl2anc	$⊢ φ \to W \in NrmCVec$
58	4 53	nvgcl	$⊢ (W \in NrmCVec \land K \in Y \land L \in Y) \to K +_{v} (W) L \in Y$
59	57 14 15 58	syl3anc	$⊢ φ \to K +_{v} (W) L \in Y$
60	55 59	eqeltrrd	$⊢ φ \to K +_{v} (U) L \in Y$
61		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
62		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
63	4 61 62 40	sspsval	$⊢ ((U \in NrmCVec \land W \in SubSp (U)) \land (\frac{1}{2} \in ℂ \land K +_{v} (U) L \in Y)) \to (\frac{1}{2}) \cdot_{𝑠OLD} (W) (K +_{v} (U) L) = (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)$
64	35 39 51 60 63	syl22anc	$⊢ φ \to (\frac{1}{2}) \cdot_{𝑠OLD} (W) (K +_{v} (U) L) = (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)$
65	4 62	nvscl	$⊢ (W \in NrmCVec \land \frac{1}{2} \in ℂ \land K +_{v} (U) L \in Y) \to (\frac{1}{2}) \cdot_{𝑠OLD} (W) (K +_{v} (U) L) \in Y$
66	57 51 60 65	syl3anc	$⊢ φ \to (\frac{1}{2}) \cdot_{𝑠OLD} (W) (K +_{v} (U) L) \in Y$
67	64 66	eqeltrrd	$⊢ φ \to (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \in Y$
68	42 67	sseldd	$⊢ φ \to (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \in X$
69	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \in X) \to A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)) \in X$
70	35 7 68 69	syl3anc	$⊢ φ \to A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)) \in X$
71	1 3	nvcl	$⊢ (U \in NrmCVec \land A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)) \in X) \to N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ℝ$
72	35 70 71	syl2anc	$⊢ φ \to N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ℝ$
73	72	resqcld	$⊢ φ \to {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ$
74		remulcl	$⊢ (4 \in ℝ \land {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ) \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ$
75	18 73 74	sylancr	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ$
76	75 47	readdcld	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} + {(K D L)}^{2} \in ℝ$
77	31 12	readdcld	$⊢ φ \to S^{2} + B \in ℝ$
78		remulcl	$⊢ (4 \in ℝ \land S^{2} + B \in ℝ) \to 4 (S^{2} + B) \in ℝ$
79	18 77 78	sylancr	$⊢ φ \to 4 (S^{2} + B) \in ℝ$
80	22	a1i	$⊢ φ \to 0 \in ℝ$
81		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)$
82	20 21 27 80 81	syl31anc	$⊢ φ \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
83	23 82	mpbird	$⊢ φ \to 0 \leq inf (R ℝ <)$
84	83 11	breqtrrdi	$⊢ φ \to 0 \leq S$
85		eqid	$⊢ N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
86		oveq2	$⊢ y = (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \to A M y = A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))$
87	86	fveq2d	$⊢ y = (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \to N (A M y) = N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
88	87	rspceeqv	$⊢ ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \in Y \land N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))) \to \exists y \in Y N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N (A M y)$
89	67 85 88	sylancl	$⊢ φ \to \exists y \in Y N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N (A M y)$
90		eqid	$⊢ (y \in Y ⟼ N (A M y)) = (y \in Y ⟼ N (A M y))$
91		fvex	$⊢ N (A M y) \in V$
92	90 91	elrnmpti	$⊢ N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ran (y \in Y ⟼ N (A M y)) \leftrightarrow \exists y \in Y N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N (A M y)$
93	89 92	sylibr	$⊢ φ \to N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ran (y \in Y ⟼ N (A M y))$
94	93 10	eleqtrrdi	$⊢ φ \to N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in R$
95		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall w \in R x \leq w \land N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in R) \to inf (R ℝ <) \leq N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
96	20 27 94 95	syl3anc	$⊢ φ \to inf (R ℝ <) \leq N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
97	11 96	eqbrtrid	$⊢ φ \to S \leq N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
98		le2sq2	$⊢ ((S \in ℝ \land 0 \leq S) \land (N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ℝ \land S \leq N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))))) \to S^{2} \leq {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
99	30 84 72 97 98	syl22anc	$⊢ φ \to S^{2} \leq {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
100		4pos	$⊢ 0 < 4$
101	18 100	pm3.2i	$⊢ (4 \in ℝ \land 0 < 4)$
102		lemul2	$⊢ (S^{2} \in ℝ \land {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ \land (4 \in ℝ \land 0 < 4)) \to (S^{2} \leq {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2})$
103	101 102	mp3an3	$⊢ (S^{2} \in ℝ \land {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \in ℝ) \to (S^{2} \leq {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2})$
104	31 73 103	syl2anc	$⊢ φ \to (S^{2} \leq {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2})$
105	99 104	mpbid	$⊢ φ \to 4 S^{2} \leq 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
106	33 75 47 105	leadd1dd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} + {(K D L)}^{2}$
107		metcl	$⊢ (D \in Met (X) \land A \in X \land K \in X) \to A D K \in ℝ$
108	37 7 43 107	syl3anc	$⊢ φ \to A D K \in ℝ$
109	108	resqcld	$⊢ φ \to {(A D K)}^{2} \in ℝ$
110		metcl	$⊢ (D \in Met (X) \land A \in X \land L \in X) \to A D L \in ℝ$
111	37 7 44 110	syl3anc	$⊢ φ \to A D L \in ℝ$
112	111	resqcld	$⊢ φ \to {(A D L)}^{2} \in ℝ$
113	109 112 77 77 16 17	le2addd	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} \leq S^{2} + B + S^{2} + B$
114	77	recnd	$⊢ φ \to S^{2} + B \in ℂ$
115	114	2timesd	$⊢ φ \to 2 (S^{2} + B) = S^{2} + B + S^{2} + B$
116	113 115	breqtrrd	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} \leq 2 (S^{2} + B)$
117	109 112	readdcld	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} \in ℝ$
118		2re	$⊢ 2 \in ℝ$
119		remulcl	$⊢ (2 \in ℝ \land S^{2} + B \in ℝ) \to 2 (S^{2} + B) \in ℝ$
120	118 77 119	sylancr	$⊢ φ \to 2 (S^{2} + B) \in ℝ$
121		2pos	$⊢ 0 < 2$
122	118 121	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
123		lemul2	$⊢ ({(A D K)}^{2} + {(A D L)}^{2} \in ℝ \land 2 (S^{2} + B) \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ({(A D K)}^{2} + {(A D L)}^{2} \leq 2 (S^{2} + B) \leftrightarrow 2 ({(A D K)}^{2} + {(A D L)}^{2}) \leq 2 2 (S^{2} + B))$
124	122 123	mp3an3	$⊢ ({(A D K)}^{2} + {(A D L)}^{2} \in ℝ \land 2 (S^{2} + B) \in ℝ) \to ({(A D K)}^{2} + {(A D L)}^{2} \leq 2 (S^{2} + B) \leftrightarrow 2 ({(A D K)}^{2} + {(A D L)}^{2}) \leq 2 2 (S^{2} + B))$
125	117 120 124	syl2anc	$⊢ φ \to ({(A D K)}^{2} + {(A D L)}^{2} \leq 2 (S^{2} + B) \leftrightarrow 2 ({(A D K)}^{2} + {(A D L)}^{2}) \leq 2 2 (S^{2} + B))$
126	116 125	mpbid	$⊢ φ \to 2 ({(A D K)}^{2} + {(A D L)}^{2}) \leq 2 2 (S^{2} + B)$
127	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land K \in X) \to A M K \in X$
128	35 7 43 127	syl3anc	$⊢ φ \to A M K \in X$
129	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land L \in X) \to A M L \in X$
130	35 7 44 129	syl3anc	$⊢ φ \to A M L \in X$
131	1 52 2 3	phpar2	$⊢ (U \in {CPreHil}_{OLD} \land A M K \in X \land A M L \in X) \to {N ((A M K) +_{v} (U) (A M L))}^{2} + {N ((A M K) M (A M L))}^{2} = 2 ({N (A M K)}^{2} + {N (A M L)}^{2})$
132	5 128 130 131	syl3anc	$⊢ φ \to {N ((A M K) +_{v} (U) (A M L))}^{2} + {N ((A M K) M (A M L))}^{2} = 2 ({N (A M K)}^{2} + {N (A M L)}^{2})$
133		2cn	$⊢ 2 \in ℂ$
134	72	recnd	$⊢ φ \to N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ℂ$
135		sqmul	$⊢ (2 \in ℂ \land N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) \in ℂ) \to {2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = 2^{2} {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
136	133 134 135	sylancr	$⊢ φ \to {2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = 2^{2} {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
137		sq2	$⊢ 2^{2} = 4$
138	137	oveq1i	$⊢ 2^{2} {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
139	136 138	eqtrdi	$⊢ φ \to {2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2}$
140	133	a1i	$⊢ φ \to 2 \in ℂ$
141	1 61 3	nvs	$⊢ (U \in NrmCVec \land 2 \in ℂ \land A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)) \in X) \to N (2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))) = \|2\| N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
142	35 140 70 141	syl3anc	$⊢ φ \to N (2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))) = \|2\| N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
143		0le2	$⊢ 0 \leq 2$
144		absid	$⊢ (2 \in ℝ \land 0 \leq 2) \to \|2\| = 2$
145	118 143 144	mp2an	$⊢ \|2\| = 2$
146	145	oveq1i	$⊢ \|2\| N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = 2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
147	142 146	eqtrdi	$⊢ φ \to N (2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))) = 2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
148	1 2 61	nvmdi	$⊢ (U \in NrmCVec \land (2 \in ℂ \land A \in X \land (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) \in X)) \to 2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = (2 \cdot_{𝑠OLD} (U) A) M (2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
149	35 140 7 68 148	syl13anc	$⊢ φ \to 2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = (2 \cdot_{𝑠OLD} (U) A) M (2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
150	1 52 61	nv2	$⊢ (U \in NrmCVec \land A \in X) \to A +_{v} (U) A = 2 \cdot_{𝑠OLD} (U) A$
151	35 7 150	syl2anc	$⊢ φ \to A +_{v} (U) A = 2 \cdot_{𝑠OLD} (U) A$
152		2ne0	$⊢ 2 \neq 0$
153	133 152	recidi	$⊢ 2 (\frac{1}{2}) = 1$
154	153	oveq1i	$⊢ 2 (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = 1 \cdot_{𝑠OLD} (U) (K +_{v} (U) L)$
155	1 52	nvgcl	$⊢ (U \in NrmCVec \land K \in X \land L \in X) \to K +_{v} (U) L \in X$
156	35 43 44 155	syl3anc	$⊢ φ \to K +_{v} (U) L \in X$
157	1 61	nvsid	$⊢ (U \in NrmCVec \land K +_{v} (U) L \in X) \to 1 \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = K +_{v} (U) L$
158	35 156 157	syl2anc	$⊢ φ \to 1 \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = K +_{v} (U) L$
159	154 158	eqtrid	$⊢ φ \to 2 (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = K +_{v} (U) L$
160	1 61	nvsass	$⊢ (U \in NrmCVec \land (2 \in ℂ \land \frac{1}{2} \in ℂ \land K +_{v} (U) L \in X)) \to 2 (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = 2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))$
161	35 140 51 156 160	syl13anc	$⊢ φ \to 2 (\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L) = 2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))$
162	159 161	eqtr3d	$⊢ φ \to K +_{v} (U) L = 2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))$
163	151 162	oveq12d	$⊢ φ \to (A +_{v} (U) A) M (K +_{v} (U) L) = (2 \cdot_{𝑠OLD} (U) A) M (2 \cdot_{𝑠OLD} (U) ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))$
164	1 52 2	nvaddsub4	$⊢ (U \in NrmCVec \land (A \in X \land A \in X) \land (K \in X \land L \in X)) \to (A +_{v} (U) A) M (K +_{v} (U) L) = (A M K) +_{v} (U) (A M L)$
165	35 7 7 43 44 164	syl122anc	$⊢ φ \to (A +_{v} (U) A) M (K +_{v} (U) L) = (A M K) +_{v} (U) (A M L)$
166	149 163 165	3eqtr2d	$⊢ φ \to 2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = (A M K) +_{v} (U) (A M L)$
167	166	fveq2d	$⊢ φ \to N (2 \cdot_{𝑠OLD} (U) (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))) = N ((A M K) +_{v} (U) (A M L))$
168	147 167	eqtr3d	$⊢ φ \to 2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L))) = N ((A M K) +_{v} (U) (A M L))$
169	168	oveq1d	$⊢ φ \to {2 N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = {N ((A M K) +_{v} (U) (A M L))}^{2}$
170	139 169	eqtr3d	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} = {N ((A M K) +_{v} (U) (A M L))}^{2}$
171	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land L \in X \land K \in X) \to L D K = N (L M K)$
172	35 44 43 171	syl3anc	$⊢ φ \to L D K = N (L M K)$
173		metsym	$⊢ (D \in Met (X) \land K \in X \land L \in X) \to K D L = L D K$
174	37 43 44 173	syl3anc	$⊢ φ \to K D L = L D K$
175	1 2	nvnnncan1	$⊢ (U \in NrmCVec \land (A \in X \land K \in X \land L \in X)) \to (A M K) M (A M L) = L M K$
176	35 7 43 44 175	syl13anc	$⊢ φ \to (A M K) M (A M L) = L M K$
177	176	fveq2d	$⊢ φ \to N ((A M K) M (A M L)) = N (L M K)$
178	172 174 177	3eqtr4d	$⊢ φ \to K D L = N ((A M K) M (A M L))$
179	178	oveq1d	$⊢ φ \to {(K D L)}^{2} = {N ((A M K) M (A M L))}^{2}$
180	170 179	oveq12d	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} + {(K D L)}^{2} = {N ((A M K) +_{v} (U) (A M L))}^{2} + {N ((A M K) M (A M L))}^{2}$
181	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land A \in X \land K \in X) \to A D K = N (A M K)$
182	35 7 43 181	syl3anc	$⊢ φ \to A D K = N (A M K)$
183	182	oveq1d	$⊢ φ \to {(A D K)}^{2} = {N (A M K)}^{2}$
184	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land A \in X \land L \in X) \to A D L = N (A M L)$
185	35 7 44 184	syl3anc	$⊢ φ \to A D L = N (A M L)$
186	185	oveq1d	$⊢ φ \to {(A D L)}^{2} = {N (A M L)}^{2}$
187	183 186	oveq12d	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} = {N (A M K)}^{2} + {N (A M L)}^{2}$
188	187	oveq2d	$⊢ φ \to 2 ({(A D K)}^{2} + {(A D L)}^{2}) = 2 ({N (A M K)}^{2} + {N (A M L)}^{2})$
189	132 180 188	3eqtr4d	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} + {(K D L)}^{2} = 2 ({(A D K)}^{2} + {(A D L)}^{2})$
190		2t2e4	$⊢ 2 \cdot 2 = 4$
191	190	oveq1i	$⊢ 2 \cdot 2 (S^{2} + B) = 4 (S^{2} + B)$
192	140 140 114	mulassd	$⊢ φ \to 2 \cdot 2 (S^{2} + B) = 2 2 (S^{2} + B)$
193	191 192	eqtr3id	$⊢ φ \to 4 (S^{2} + B) = 2 2 (S^{2} + B)$
194	126 189 193	3brtr4d	$⊢ φ \to 4 {N (A M ((\frac{1}{2}) \cdot_{𝑠OLD} (U) (K +_{v} (U) L)))}^{2} + {(K D L)}^{2} \leq 4 (S^{2} + B)$
195	48 76 79 106 194	letrd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 (S^{2} + B)$
196		4cn	$⊢ 4 \in ℂ$
197	196	a1i	$⊢ φ \to 4 \in ℂ$
198	31	recnd	$⊢ φ \to S^{2} \in ℂ$
199	12	recnd	$⊢ φ \to B \in ℂ$
200	197 198 199	adddid	$⊢ φ \to 4 (S^{2} + B) = 4 S^{2} + 4 B$
201	195 200	breqtrd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 S^{2} + 4 B$
202		remulcl	$⊢ (4 \in ℝ \land B \in ℝ) \to 4 B \in ℝ$
203	18 12 202	sylancr	$⊢ φ \to 4 B \in ℝ$
204	47 203 33	leadd2d	$⊢ φ \to ({(K D L)}^{2} \leq 4 B \leftrightarrow 4 S^{2} + {(K D L)}^{2} \leq 4 S^{2} + 4 B)$
205	201 204	mpbird	$⊢ φ \to {(K D L)}^{2} \leq 4 B$

Metamath Proof Explorer

Theorem minvecolem2

Proof