minveclem2

Description: Lemma for minvec . 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 Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

	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)}$
	minveclem2.1	$⊢ φ \to B \in ℝ$
	minveclem2.2	$⊢ φ \to 0 \leq B$
	minveclem2.3	$⊢ φ \to K \in Y$
	minveclem2.4	$⊢ φ \to L \in Y$
	minveclem2.5	$⊢ φ \to {(A D K)}^{2} \leq S^{2} + B$
	minveclem2.6	$⊢ φ \to {(A D L)}^{2} \leq S^{2} + B$
Assertion	minveclem2	$⊢ φ \to {(K D L)}^{2} \leq 4 B$

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		minveclem2.1	$⊢ φ \to B \in ℝ$
13		minveclem2.2	$⊢ φ \to 0 \leq B$
14		minveclem2.3	$⊢ φ \to K \in Y$
15		minveclem2.4	$⊢ φ \to L \in Y$
16		minveclem2.5	$⊢ φ \to {(A D K)}^{2} \leq S^{2} + B$
17		minveclem2.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	minveclem4c	$⊢ φ \to S \in ℝ$
20	19	resqcld	$⊢ φ \to S^{2} \in ℝ$
21		remulcl	$⊢ (4 \in ℝ \land S^{2} \in ℝ) \to 4 S^{2} \in ℝ$
22	18 20 21	sylancr	$⊢ φ \to 4 S^{2} \in ℝ$
23		cphngp	$⊢ U \in CPreHil \to U \in NrmGrp$
24	4 23	syl	$⊢ φ \to U \in NrmGrp$
25		ngpms	$⊢ U \in NrmGrp \to U \in MetSp$
26	24 25	syl	$⊢ φ \to U \in MetSp$
27	1 11	msmet	$⊢ U \in MetSp \to D \in Met (X)$
28	26 27	syl	$⊢ φ \to D \in Met (X)$
29		eqid	$⊢ LSubSp (U) = LSubSp (U)$
30	1 29	lssss	$⊢ Y \in LSubSp (U) \to Y \subseteq X$
31	5 30	syl	$⊢ φ \to Y \subseteq X$
32	31 14	sseldd	$⊢ φ \to K \in X$
33	31 15	sseldd	$⊢ φ \to L \in X$
34		metcl	$⊢ (D \in Met (X) \land K \in X \land L \in X) \to K D L \in ℝ$
35	28 32 33 34	syl3anc	$⊢ φ \to K D L \in ℝ$
36	35	resqcld	$⊢ φ \to {(K D L)}^{2} \in ℝ$
37	22 36	readdcld	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \in ℝ$
38		cphlmod	$⊢ U \in CPreHil \to U \in LMod$
39	4 38	syl	$⊢ φ \to U \in LMod$
40		cphclm	$⊢ U \in CPreHil \to U \in CMod$
41	4 40	syl	$⊢ φ \to U \in CMod$
42		eqid	$⊢ Scalar (U) = Scalar (U)$
43		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
44	42 43	clmzss	$⊢ U \in CMod \to ℤ \subseteq {Base}_{Scalar (U)}$
45	41 44	syl	$⊢ φ \to ℤ \subseteq {Base}_{Scalar (U)}$
46		2z	$⊢ 2 \in ℤ$
47	46	a1i	$⊢ φ \to 2 \in ℤ$
48	45 47	sseldd	$⊢ φ \to 2 \in {Base}_{Scalar (U)}$
49		2ne0	$⊢ 2 \neq 0$
50	49	a1i	$⊢ φ \to 2 \neq 0$
51	42 43	cphreccl	$⊢ (U \in CPreHil \land 2 \in {Base}_{Scalar (U)} \land 2 \neq 0) \to \frac{1}{2} \in {Base}_{Scalar (U)}$
52	4 48 50 51	syl3anc	$⊢ φ \to \frac{1}{2} \in {Base}_{Scalar (U)}$
53		eqid	$⊢ +_{U} = +_{U}$
54	53 29	lssvacl	$⊢ ((U \in LMod \land Y \in LSubSp (U)) \land (K \in Y \land L \in Y)) \to K +_{U} L \in Y$
55	39 5 14 15 54	syl22anc	$⊢ φ \to K +_{U} L \in Y$
56		eqid	$⊢ \cdot_{U} = \cdot_{U}$
57	42 56 43 29	lssvscl	$⊢ ((U \in LMod \land Y \in LSubSp (U)) \land (\frac{1}{2} \in {Base}_{Scalar (U)} \land K +_{U} L \in Y)) \to (\frac{1}{2}) \cdot_{U} (K +_{U} L) \in Y$
58	39 5 52 55 57	syl22anc	$⊢ φ \to (\frac{1}{2}) \cdot_{U} (K +_{U} L) \in Y$
59	31 58	sseldd	$⊢ φ \to (\frac{1}{2}) \cdot_{U} (K +_{U} L) \in X$
60	1 2	lmodvsubcl	$⊢ (U \in LMod \land A \in X \land (\frac{1}{2}) \cdot_{U} (K +_{U} L) \in X) \to A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)) \in X$
61	39 7 59 60	syl3anc	$⊢ φ \to A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)) \in X$
62	1 3	nmcl	$⊢ (U \in NrmGrp \land A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)) \in X) \to N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ℝ$
63	24 61 62	syl2anc	$⊢ φ \to N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ℝ$
64	63	resqcld	$⊢ φ \to {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ$
65		remulcl	$⊢ (4 \in ℝ \land {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ) \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ$
66	18 64 65	sylancr	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ$
67	66 36	readdcld	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} + {(K D L)}^{2} \in ℝ$
68	20 12	readdcld	$⊢ φ \to S^{2} + B \in ℝ$
69		remulcl	$⊢ (4 \in ℝ \land S^{2} + B \in ℝ) \to 4 (S^{2} + B) \in ℝ$
70	18 68 69	sylancr	$⊢ φ \to 4 (S^{2} + B) \in ℝ$
71	1 2 3 4 5 6 7 8 9	minveclem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
72	71	simp3d	$⊢ φ \to \forall w \in R 0 \leq w$
73	71	simp1d	$⊢ φ \to R \subseteq ℝ$
74	71	simp2d	$⊢ φ \to R \neq \emptyset$
75		0re	$⊢ 0 \in ℝ$
76		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
77	76	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
78	77	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
79	75 72 78	sylancr	$⊢ φ \to \exists x \in ℝ \forall w \in R x \leq w$
80	75	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	73 74 79 80 81	syl31anc	$⊢ φ \to (0 \leq inf (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
83	72 82	mpbird	$⊢ φ \to 0 \leq inf (R ℝ <)$
84	83 10	breqtrrdi	$⊢ φ \to 0 \leq S$
85		eqid	$⊢ N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
86		oveq2	$⊢ y = (\frac{1}{2}) \cdot_{U} (K +_{U} L) \to A \underset{˙}{-} y = A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))$
87	86	fveq2d	$⊢ y = (\frac{1}{2}) \cdot_{U} (K +_{U} L) \to N (A \underset{˙}{-} y) = N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
88	87	rspceeqv	$⊢ ((\frac{1}{2}) \cdot_{U} (K +_{U} L) \in Y \land N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))) \to \exists y \in Y N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N (A \underset{˙}{-} y)$
89	58 85 88	sylancl	$⊢ φ \to \exists y \in Y N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N (A \underset{˙}{-} y)$
90		eqid	$⊢ (y \in Y ⟼ N (A \underset{˙}{-} y)) = (y \in Y ⟼ N (A \underset{˙}{-} y))$
91		fvex	$⊢ N (A \underset{˙}{-} y) \in V$
92	90 91	elrnmpti	$⊢ N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ran (y \in Y ⟼ N (A \underset{˙}{-} y)) \leftrightarrow \exists y \in Y N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N (A \underset{˙}{-} y)$
93	89 92	sylibr	$⊢ φ \to N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ran (y \in Y ⟼ N (A \underset{˙}{-} y))$
94	93 9	eleqtrrdi	$⊢ φ \to N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in R$
95		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall w \in R x \leq w \land N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in R) \to inf (R ℝ <) \leq N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
96	73 79 94 95	syl3anc	$⊢ φ \to inf (R ℝ <) \leq N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
97	10 96	eqbrtrid	$⊢ φ \to S \leq N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
98		le2sq2	$⊢ ((S \in ℝ \land 0 \leq S) \land (N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ℝ \land S \leq N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))))) \to S^{2} \leq {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
99	19 84 63 97 98	syl22anc	$⊢ φ \to S^{2} \leq {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{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 \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ \land (4 \in ℝ \land 0 < 4)) \to (S^{2} \leq {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2})$
103	101 102	mp3an3	$⊢ (S^{2} \in ℝ \land {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \in ℝ) \to (S^{2} \leq {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2})$
104	20 64 103	syl2anc	$⊢ φ \to (S^{2} \leq {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} \leftrightarrow 4 S^{2} \leq 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2})$
105	99 104	mpbid	$⊢ φ \to 4 S^{2} \leq 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
106	22 66 36 105	leadd1dd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{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	28 7 32 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	28 7 33 110	syl3anc	$⊢ φ \to A D L \in ℝ$
112	111	resqcld	$⊢ φ \to {(A D L)}^{2} \in ℝ$
113	109 112 68 68 16 17	le2addd	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} \leq S^{2} + B + S^{2} + B$
114	68	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 68 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	lmodvsubcl	$⊢ (U \in LMod \land A \in X \land K \in X) \to A \underset{˙}{-} K \in X$
128	39 7 32 127	syl3anc	$⊢ φ \to A \underset{˙}{-} K \in X$
129	1 2	lmodvsubcl	$⊢ (U \in LMod \land A \in X \land L \in X) \to A \underset{˙}{-} L \in X$
130	39 7 33 129	syl3anc	$⊢ φ \to A \underset{˙}{-} L \in X$
131	1 53 2 3	nmpar	$⊢ (U \in CPreHil \land A \underset{˙}{-} K \in X \land A \underset{˙}{-} L \in X) \to {N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))}^{2} + {N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L))}^{2} = 2 ({N (A \underset{˙}{-} K)}^{2} + {N (A \underset{˙}{-} L)}^{2})$
132	4 128 130 131	syl3anc	$⊢ φ \to {N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))}^{2} + {N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L))}^{2} = 2 ({N (A \underset{˙}{-} K)}^{2} + {N (A \underset{˙}{-} L)}^{2})$
133		2cn	$⊢ 2 \in ℂ$
134	63	recnd	$⊢ φ \to N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ℂ$
135		sqmul	$⊢ (2 \in ℂ \land N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) \in ℂ) \to {2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = 2^{2} {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
136	133 134 135	sylancr	$⊢ φ \to {2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = 2^{2} {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
137		sq2	$⊢ 2^{2} = 4$
138	137	oveq1i	$⊢ 2^{2} {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
139	136 138	eqtrdi	$⊢ φ \to {2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2}$
140	1 3 56 42 43	cphnmvs	$⊢ (U \in CPreHil \land 2 \in {Base}_{Scalar (U)} \land A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)) \in X) \to N (2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))) = \|2\| N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
141	4 48 61 140	syl3anc	$⊢ φ \to N (2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))) = \|2\| N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
142		0le2	$⊢ 0 \leq 2$
143		absid	$⊢ (2 \in ℝ \land 0 \leq 2) \to \|2\| = 2$
144	118 142 143	mp2an	$⊢ \|2\| = 2$
145	144	oveq1i	$⊢ \|2\| N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = 2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
146	141 145	eqtrdi	$⊢ φ \to N (2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))) = 2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
147	1 56 42 43 2 39 48 7 59	lmodsubdi	$⊢ φ \to 2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = (2 \cdot_{U} A) \underset{˙}{-} (2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
148		eqid	$⊢ \cdot_{U} = \cdot_{U}$
149	1 148 53	mulg2	$⊢ A \in X \to 2 \cdot_{U} A = A +_{U} A$
150	7 149	syl	$⊢ φ \to 2 \cdot_{U} A = A +_{U} A$
151	1 148 56	clmmulg	$⊢ (U \in CMod \land 2 \in ℤ \land A \in X) \to 2 \cdot_{U} A = 2 \cdot_{U} A$
152	41 47 7 151	syl3anc	$⊢ φ \to 2 \cdot_{U} A = 2 \cdot_{U} A$
153	150 152	eqtr3d	$⊢ φ \to A +_{U} A = 2 \cdot_{U} A$
154	1 53	lmodvacl	$⊢ (U \in LMod \land K \in X \land L \in X) \to K +_{U} L \in X$
155	39 32 33 154	syl3anc	$⊢ φ \to K +_{U} L \in X$
156	1 56	clmvs1	$⊢ (U \in CMod \land K +_{U} L \in X) \to 1 \cdot_{U} (K +_{U} L) = K +_{U} L$
157	41 155 156	syl2anc	$⊢ φ \to 1 \cdot_{U} (K +_{U} L) = K +_{U} L$
158	133 49	recidi	$⊢ 2 (\frac{1}{2}) = 1$
159	158	oveq1i	$⊢ 2 (\frac{1}{2}) \cdot_{U} (K +_{U} L) = 1 \cdot_{U} (K +_{U} L)$
160	1 42 56 43	clmvsass	$⊢ (U \in CMod \land (2 \in {Base}_{Scalar (U)} \land \frac{1}{2} \in {Base}_{Scalar (U)} \land K +_{U} L \in X)) \to 2 (\frac{1}{2}) \cdot_{U} (K +_{U} L) = 2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))$
161	41 48 52 155 160	syl13anc	$⊢ φ \to 2 (\frac{1}{2}) \cdot_{U} (K +_{U} L) = 2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))$
162	159 161	eqtr3id	$⊢ φ \to 1 \cdot_{U} (K +_{U} L) = 2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))$
163	157 162	eqtr3d	$⊢ φ \to K +_{U} L = 2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))$
164	153 163	oveq12d	$⊢ φ \to (A +_{U} A) \underset{˙}{-} (K +_{U} L) = (2 \cdot_{U} A) \underset{˙}{-} (2 \cdot_{U} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))$
165		lmodabl	$⊢ U \in LMod \to U \in Abel$
166	39 165	syl	$⊢ φ \to U \in Abel$
167	1 53 2	ablsub4	$⊢ (U \in Abel \land (A \in X \land A \in X) \land (K \in X \land L \in X)) \to (A +_{U} A) \underset{˙}{-} (K +_{U} L) = (A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L)$
168	166 7 7 32 33 167	syl122anc	$⊢ φ \to (A +_{U} A) \underset{˙}{-} (K +_{U} L) = (A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L)$
169	147 164 168	3eqtr2d	$⊢ φ \to 2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = (A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L)$
170	169	fveq2d	$⊢ φ \to N (2 \cdot_{U} (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))) = N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))$
171	146 170	eqtr3d	$⊢ φ \to 2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L))) = N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))$
172	171	oveq1d	$⊢ φ \to {2 N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = {N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))}^{2}$
173	139 172	eqtr3d	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} = {N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))}^{2}$
174		eqid	$⊢ dist (U) = dist (U)$
175	3 1 2 174	ngpdsr	$⊢ (U \in NrmGrp \land K \in X \land L \in X) \to K dist (U) L = N (L \underset{˙}{-} K)$
176	24 32 33 175	syl3anc	$⊢ φ \to K dist (U) L = N (L \underset{˙}{-} K)$
177	11	oveqi	$⊢ K D L = K ({dist (U) ↾}_{(X \times X)}) L$
178	32 33	ovresd	$⊢ φ \to K ({dist (U) ↾}_{(X \times X)}) L = K dist (U) L$
179	177 178	eqtrid	$⊢ φ \to K D L = K dist (U) L$
180	1 2 166 7 32 33	ablnnncan1	$⊢ φ \to (A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L) = L \underset{˙}{-} K$
181	180	fveq2d	$⊢ φ \to N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L)) = N (L \underset{˙}{-} K)$
182	176 179 181	3eqtr4d	$⊢ φ \to K D L = N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L))$
183	182	oveq1d	$⊢ φ \to {(K D L)}^{2} = {N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L))}^{2}$
184	173 183	oveq12d	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} + {(K D L)}^{2} = {N ((A \underset{˙}{-} K) +_{U} (A \underset{˙}{-} L))}^{2} + {N ((A \underset{˙}{-} K) \underset{˙}{-} (A \underset{˙}{-} L))}^{2}$
185	11	oveqi	$⊢ A D K = A ({dist (U) ↾}_{(X \times X)}) K$
186	7 32	ovresd	$⊢ φ \to A ({dist (U) ↾}_{(X \times X)}) K = A dist (U) K$
187	185 186	eqtrid	$⊢ φ \to A D K = A dist (U) K$
188	3 1 2 174	ngpds	$⊢ (U \in NrmGrp \land A \in X \land K \in X) \to A dist (U) K = N (A \underset{˙}{-} K)$
189	24 7 32 188	syl3anc	$⊢ φ \to A dist (U) K = N (A \underset{˙}{-} K)$
190	187 189	eqtrd	$⊢ φ \to A D K = N (A \underset{˙}{-} K)$
191	190	oveq1d	$⊢ φ \to {(A D K)}^{2} = {N (A \underset{˙}{-} K)}^{2}$
192	11	oveqi	$⊢ A D L = A ({dist (U) ↾}_{(X \times X)}) L$
193	7 33	ovresd	$⊢ φ \to A ({dist (U) ↾}_{(X \times X)}) L = A dist (U) L$
194	192 193	eqtrid	$⊢ φ \to A D L = A dist (U) L$
195	3 1 2 174	ngpds	$⊢ (U \in NrmGrp \land A \in X \land L \in X) \to A dist (U) L = N (A \underset{˙}{-} L)$
196	24 7 33 195	syl3anc	$⊢ φ \to A dist (U) L = N (A \underset{˙}{-} L)$
197	194 196	eqtrd	$⊢ φ \to A D L = N (A \underset{˙}{-} L)$
198	197	oveq1d	$⊢ φ \to {(A D L)}^{2} = {N (A \underset{˙}{-} L)}^{2}$
199	191 198	oveq12d	$⊢ φ \to {(A D K)}^{2} + {(A D L)}^{2} = {N (A \underset{˙}{-} K)}^{2} + {N (A \underset{˙}{-} L)}^{2}$
200	199	oveq2d	$⊢ φ \to 2 ({(A D K)}^{2} + {(A D L)}^{2}) = 2 ({N (A \underset{˙}{-} K)}^{2} + {N (A \underset{˙}{-} L)}^{2})$
201	132 184 200	3eqtr4d	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} + {(K D L)}^{2} = 2 ({(A D K)}^{2} + {(A D L)}^{2})$
202		2t2e4	$⊢ 2 \cdot 2 = 4$
203	202	oveq1i	$⊢ 2 \cdot 2 (S^{2} + B) = 4 (S^{2} + B)$
204		2cnd	$⊢ φ \to 2 \in ℂ$
205	204 204 114	mulassd	$⊢ φ \to 2 \cdot 2 (S^{2} + B) = 2 2 (S^{2} + B)$
206	203 205	eqtr3id	$⊢ φ \to 4 (S^{2} + B) = 2 2 (S^{2} + B)$
207	126 201 206	3brtr4d	$⊢ φ \to 4 {N (A \underset{˙}{-} ((\frac{1}{2}) \cdot_{U} (K +_{U} L)))}^{2} + {(K D L)}^{2} \leq 4 (S^{2} + B)$
208	37 67 70 106 207	letrd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 (S^{2} + B)$
209		4cn	$⊢ 4 \in ℂ$
210	209	a1i	$⊢ φ \to 4 \in ℂ$
211	20	recnd	$⊢ φ \to S^{2} \in ℂ$
212	12	recnd	$⊢ φ \to B \in ℂ$
213	210 211 212	adddid	$⊢ φ \to 4 (S^{2} + B) = 4 S^{2} + 4 B$
214	208 213	breqtrd	$⊢ φ \to 4 S^{2} + {(K D L)}^{2} \leq 4 S^{2} + 4 B$
215		remulcl	$⊢ (4 \in ℝ \land B \in ℝ) \to 4 B \in ℝ$
216	18 12 215	sylancr	$⊢ φ \to 4 B \in ℝ$
217	36 216 22	leadd2d	$⊢ φ \to ({(K D L)}^{2} \leq 4 B \leftrightarrow 4 S^{2} + {(K D L)}^{2} \leq 4 S^{2} + 4 B)$
218	214 217	mpbird	$⊢ φ \to {(K D L)}^{2} \leq 4 B$

Metamath Proof Explorer

Theorem minveclem2

Proof