Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( Base ‘ 𝑈 )
minvec.m ⊢ − = ( -g ‘ 𝑈 )
minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
minveclem2.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
minveclem2.2 ⊢ ( 𝜑 → 0 ≤ 𝐵 )
minveclem2.3 ⊢ ( 𝜑 → 𝐾 ∈ 𝑌 )
minveclem2.4 ⊢ ( 𝜑 → 𝐿 ∈ 𝑌 )
minveclem2.5 ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
minveclem2.6 ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
Assertion minveclem2 ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
2 minvec.m ⊢ − = ( -g ‘ 𝑈 )
3 minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
4 minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5 minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6 minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7 minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
9 minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
10 minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
12 minveclem2.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
13 minveclem2.2 ⊢ ( 𝜑 → 0 ≤ 𝐵 )
14 minveclem2.3 ⊢ ( 𝜑 → 𝐾 ∈ 𝑌 )
15 minveclem2.4 ⊢ ( 𝜑 → 𝐿 ∈ 𝑌 )
16 minveclem2.5 ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
17 minveclem2.6 ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
18 4re ⊢ 4 ∈ ℝ
19 1 2 3 4 5 6 7 8 9 10 minveclem4c ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
20 19 resqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ )
21 remulcl ⊢ ( ( 4 ∈ ℝ ∧ ( 𝑆 ↑ 2 ) ∈ ℝ ) → ( 4 · ( 𝑆 ↑ 2 ) ) ∈ ℝ )
22 18 20 21 sylancr ⊢ ( 𝜑 → ( 4 · ( 𝑆 ↑ 2 ) ) ∈ ℝ )
23 cphngp ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
24 4 23 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmGrp )
25 ngpms ⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp )
26 24 25 syl ⊢ ( 𝜑 → 𝑈 ∈ MetSp )
27 1 11 msmet ⊢ ( 𝑈 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
28 26 27 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
29 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
30 1 29 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
31 5 30 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
32 31 14 sseldd ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
33 31 15 sseldd ⊢ ( 𝜑 → 𝐿 ∈ 𝑋 )
34 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
35 28 32 33 34 syl3anc ⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
36 35 resqcld ⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
37 22 36 readdcld ⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
38 cphlmod ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ LMod )
39 4 38 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
40 cphclm ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ ℂMod )
41 4 40 syl ⊢ ( 𝜑 → 𝑈 ∈ ℂMod )
42 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
43 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
44 42 43 clmzss ⊢ ( 𝑈 ∈ ℂMod → ℤ ⊆ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
45 41 44 syl ⊢ ( 𝜑 → ℤ ⊆ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
46 2z ⊢ 2 ∈ ℤ
47 46 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
48 45 47 sseldd ⊢ ( 𝜑 → 2 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
49 2ne0 ⊢ 2 ≠ 0
50 49 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
51 42 43 cphreccl ⊢ ( ( 𝑈 ∈ ℂPreHil ∧ 2 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 2 ≠ 0 ) → ( 1 / 2 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
52 4 48 50 51 syl3anc ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
53 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
54 53 29 lssvacl ⊢ ( ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌 ) ) → ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 )
55 39 5 14 15 54 syl22anc ⊢ ( 𝜑 → ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 )
56 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
57 42 56 43 29 lssvscl ⊢ ( ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( 1 / 2 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 ) ) → ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 )
58 39 5 52 55 57 syl22anc ⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 )
59 31 58 sseldd ⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑋 )
60 1 2 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑋 ) → ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 )
61 39 7 59 60 syl3anc ⊢ ( 𝜑 → ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 )
62 1 3 nmcl ⊢ ( ( 𝑈 ∈ NrmGrp ∧ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ )
63 24 61 62 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ )
64 63 resqcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ )
65 remulcl ⊢ ( ( 4 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) → ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
66 18 64 65 sylancr ⊢ ( 𝜑 → ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
67 66 36 readdcld ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
68 20 12 readdcld ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ )
69 remulcl ⊢ ( ( 4 ∈ ℝ ∧ ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ ) → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
70 18 68 69 sylancr ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
71 1 2 3 4 5 6 7 8 9 minveclem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
72 71 simp3d ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
73 71 simp1d ⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
74 71 simp2d ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
75 0re ⊢ 0 ∈ ℝ
76 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
77 76 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
78 77 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
79 75 72 78 sylancr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
80 75 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
81 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
82 73 74 79 80 81 syl31anc ⊢ ( 𝜑 → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
83 72 82 mpbird ⊢ ( 𝜑 → 0 ≤ inf ( 𝑅 , ℝ , < ) )
84 83 10 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑆 )
85 eqid ⊢ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
86 oveq2 ⊢ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) → ( 𝐴 − 𝑦 ) = ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
87 86 fveq2d ⊢ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) → ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
88 87 rspceeqv ⊢ ( ( ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 ∧ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) → ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
89 58 85 88 sylancl ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
90 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
91 fvex ⊢ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ∈ V
92 90 91 elrnmpti ⊢ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
93 89 92 sylibr ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) ) )
94 93 9 eleqtrrdi ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ 𝑅 )
95 infrelb ⊢ ( ( 𝑅 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ 𝑅 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
96 73 79 94 95 syl3anc ⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
97 10 96 eqbrtrid ⊢ ( 𝜑 → 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
98 le2sq2 ⊢ ( ( ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) ∧ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ ∧ 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) ) → ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
99 19 84 63 97 98 syl22anc ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
100 4pos ⊢ 0 < 4
101 18 100 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 0 < 4 )
102 lemul2 ⊢ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
103 101 102 mp3an3 ⊢ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
104 20 64 103 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
105 99 104 mpbid ⊢ ( 𝜑 → ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
106 22 66 36 105 leadd1dd ⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) )
107 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
108 28 7 32 107 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
109 108 resqcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ∈ ℝ )
110 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
111 28 7 33 110 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
112 111 resqcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
113 109 112 68 68 16 17 le2addd ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( ( 𝑆 ↑ 2 ) + 𝐵 ) + ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
114 68 recnd ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℂ )
115 114 2timesd ⊢ ( 𝜑 → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( ( ( 𝑆 ↑ 2 ) + 𝐵 ) + ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
116 113 115 breqtrrd ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
117 109 112 readdcld ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
118 2re ⊢ 2 ∈ ℝ
119 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ ) → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
120 118 68 119 sylancr ⊢ ( 𝜑 → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
121 2pos ⊢ 0 < 2
122 118 121 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
123 lemul2 ⊢ ( ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ ∧ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
124 122 123 mp3an3 ⊢ ( ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ ∧ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ ) → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
125 117 120 124 syl2anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
126 116 125 mpbid ⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
127 1 2 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 − 𝐾 ) ∈ 𝑋 )
128 39 7 32 127 syl3anc ⊢ ( 𝜑 → ( 𝐴 − 𝐾 ) ∈ 𝑋 )
129 1 2 lmodvsubcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 − 𝐿 ) ∈ 𝑋 )
130 39 7 33 129 syl3anc ⊢ ( 𝜑 → ( 𝐴 − 𝐿 ) ∈ 𝑋 )
131 1 53 2 3 nmpar ⊢ ( ( 𝑈 ∈ ℂPreHil ∧ ( 𝐴 − 𝐾 ) ∈ 𝑋 ∧ ( 𝐴 − 𝐿 ) ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) ↑ 2 ) ) ) )
132 4 128 130 131 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) ↑ 2 ) ) ) )
133 2cn ⊢ 2 ∈ ℂ
134 63 recnd ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℂ )
135 sqmul ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℂ ) → ( ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
136 133 134 135 sylancr ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
137 sq2 ⊢ ( 2 ↑ 2 ) = 4
138 137 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
139 136 138 eqtrdi ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
140 1 3 56 42 43 cphnmvs ⊢ ( ( 𝑈 ∈ ℂPreHil ∧ 2 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
141 4 48 61 140 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
142 0le2 ⊢ 0 ≤ 2
143 absid ⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
144 118 142 143 mp2an ⊢ ( abs ‘ 2 ) = 2
145 144 oveq1i ⊢ ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
146 141 145 eqtrdi ⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
147 1 56 42 43 2 39 48 7 59 lmodsubdi ⊢ ( 𝜑 → ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( ( 2 ( ·𝑠 ‘ 𝑈 ) 𝐴 ) − ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
148 eqid ⊢ ( .g ‘ 𝑈 ) = ( .g ‘ 𝑈 )
149 1 148 53 mulg2 ⊢ ( 𝐴 ∈ 𝑋 → ( 2 ( .g ‘ 𝑈 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) )
150 7 149 syl ⊢ ( 𝜑 → ( 2 ( .g ‘ 𝑈 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) )
151 1 148 56 clmmulg ⊢ ( ( 𝑈 ∈ ℂMod ∧ 2 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝑈 ) 𝐴 ) = ( 2 ( ·𝑠 ‘ 𝑈 ) 𝐴 ) )
152 41 47 7 151 syl3anc ⊢ ( 𝜑 → ( 2 ( .g ‘ 𝑈 ) 𝐴 ) = ( 2 ( ·𝑠 ‘ 𝑈 ) 𝐴 ) )
153 150 152 eqtr3d ⊢ ( 𝜑 → ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) = ( 2 ( ·𝑠 ‘ 𝑈 ) 𝐴 ) )
154 1 53 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 )
155 39 32 33 154 syl3anc ⊢ ( 𝜑 → ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 )
156 1 56 clmvs1 ⊢ ( ( 𝑈 ∈ ℂMod ∧ ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 ) → ( 1 ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) )
157 41 155 156 syl2anc ⊢ ( 𝜑 → ( 1 ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) )
158 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
159 158 oveq1i ⊢ ( ( 2 · ( 1 / 2 ) ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 1 ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) )
160 1 42 56 43 clmvsass ⊢ ( ( 𝑈 ∈ ℂMod ∧ ( 2 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( 1 / 2 ) ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 ) ) → ( ( 2 · ( 1 / 2 ) ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
161 41 48 52 155 160 syl13anc ⊢ ( 𝜑 → ( ( 2 · ( 1 / 2 ) ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
162 159 161 eqtr3id ⊢ ( 𝜑 → ( 1 ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
163 157 162 eqtr3d ⊢ ( 𝜑 → ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) = ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) )
164 153 163 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) − ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( ( 2 ( ·𝑠 ‘ 𝑈 ) 𝐴 ) − ( 2 ( ·𝑠 ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) )
165 lmodabl ⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Abel )
166 39 165 syl ⊢ ( 𝜑 → 𝑈 ∈ Abel )
167 1 53 2 ablsub4 ⊢ ( ( 𝑈 ∈ Abel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) ) → ( ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) − ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) )
168 166 7 7 32 33 167 syl122anc ⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝑈 ) 𝐴 ) − ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) = ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) )
169 147 164 168 3eqtr2d ⊢ ( 𝜑 → ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) = ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) )
170 169 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠 ‘ 𝑈 ) ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) )
171 146 170 eqtr3d ⊢ ( 𝜑 → ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) )
172 171 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) )
173 139 172 eqtr3d ⊢ ( 𝜑 → ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) )
174 eqid ⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
175 3 1 2 174 ngpdsr ⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 ( dist ‘ 𝑈 ) 𝐿 ) = ( 𝑁 ‘ ( 𝐿 − 𝐾 ) ) )
176 24 32 33 175 syl3anc ⊢ ( 𝜑 → ( 𝐾 ( dist ‘ 𝑈 ) 𝐿 ) = ( 𝑁 ‘ ( 𝐿 − 𝐾 ) ) )
177 11 oveqi ⊢ ( 𝐾 𝐷 𝐿 ) = ( 𝐾 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐿 )
178 32 33 ovresd ⊢ ( 𝜑 → ( 𝐾 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐿 ) = ( 𝐾 ( dist ‘ 𝑈 ) 𝐿 ) )
179 177 178 eqtrid ⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) = ( 𝐾 ( dist ‘ 𝑈 ) 𝐿 ) )
180 1 2 166 7 32 33 ablnnncan1 ⊢ ( 𝜑 → ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) = ( 𝐿 − 𝐾 ) )
181 180 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) = ( 𝑁 ‘ ( 𝐿 − 𝐾 ) ) )
182 176 179 181 3eqtr4d ⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) = ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) )
183 182 oveq1d ⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) )
184 173 183 oveq12d ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) ( +g ‘ 𝑈 ) ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 − 𝐾 ) − ( 𝐴 − 𝐿 ) ) ) ↑ 2 ) ) )
185 11 oveqi ⊢ ( 𝐴 𝐷 𝐾 ) = ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐾 )
186 7 32 ovresd ⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐾 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝐾 ) )
187 185 186 eqtrid ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐾 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝐾 ) )
188 3 1 2 174 ngpds ⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝐾 ) = ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) )
189 24 7 32 188 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝑈 ) 𝐾 ) = ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) )
190 187 189 eqtrd ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐾 ) = ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) )
191 190 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) ↑ 2 ) )
192 11 oveqi ⊢ ( 𝐴 𝐷 𝐿 ) = ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐿 )
193 7 33 ovresd ⊢ ( 𝜑 → ( 𝐴 ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) 𝐿 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝐿 ) )
194 192 193 eqtrid ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐿 ) = ( 𝐴 ( dist ‘ 𝑈 ) 𝐿 ) )
195 3 1 2 174 ngpds ⊢ ( ( 𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 ( dist ‘ 𝑈 ) 𝐿 ) = ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) )
196 24 7 33 195 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝑈 ) 𝐿 ) = ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) )
197 194 196 eqtrd ⊢ ( 𝜑 → ( 𝐴 𝐷 𝐿 ) = ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) )
198 197 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) ↑ 2 ) )
199 191 198 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) ↑ 2 ) ) )
200 199 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 − 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐿 ) ) ↑ 2 ) ) ) )
201 132 184 200 3eqtr4d ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) )
202 2t2e4 ⊢ ( 2 · 2 ) = 4
203 202 oveq1i ⊢ ( ( 2 · 2 ) · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
204 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
205 204 204 114 mulassd ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
206 203 205 eqtr3id ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
207 126 201 206 3brtr4d ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 − ( ( 1 / 2 ) ( ·𝑠 ‘ 𝑈 ) ( 𝐾 ( +g ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
208 37 67 70 106 207 letrd ⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
209 4cn ⊢ 4 ∈ ℂ
210 209 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
211 20 recnd ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ )
212 12 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
213 210 211 212 adddid ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) )
214 208 213 breqtrd ⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) )
215 remulcl ⊢ ( ( 4 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 4 · 𝐵 ) ∈ ℝ )
216 18 12 215 sylancr ⊢ ( 𝜑 → ( 4 · 𝐵 ) ∈ ℝ )
217 36 216 22 leadd2d ⊢ ( 𝜑 → ( ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) ↔ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) ) )
218 214 217 mpbird ⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) )