Metamath Proof Explorer

Theorem pjthlem1

Description: Lemma for pjth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 17-Oct-2015) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Hypotheses pjthlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
pjthlem.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
pjthlem.p ⊢ + = ( +g ‘ 𝑊 )
pjthlem.m ⊢ − = ( -g ‘ 𝑊 )
pjthlem.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
pjthlem.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
pjthlem.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂHil )
pjthlem.2 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
pjthlem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pjthlem.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
pjthlem.7 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
pjthlem.8 ⊢ 𝑇 = ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) )
Assertion pjthlem1 ( 𝜑 → ( 𝐴 , 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 pjthlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 pjthlem.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 pjthlem.p ⊢ + = ( +g ‘ 𝑊 )
4 pjthlem.m ⊢ − = ( -g ‘ 𝑊 )
5 pjthlem.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
6 pjthlem.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
7 pjthlem.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂHil )
8 pjthlem.2 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
9 pjthlem.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
10 pjthlem.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
11 pjthlem.7 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) )
12 pjthlem.8 ⊢ 𝑇 = ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) )
13 hlcph ⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
14 7 13 syl ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
15 1 6 lssss ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉 )
16 8 15 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
17 16 10 sseldd ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
18 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )
19 14 9 17 18 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐵 ) ∈ ℂ )
20 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , 𝐵 ) ) ∈ ℝ )
21 20 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , 𝐵 ) ) ∈ ℂ )
22 20 resqcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ∈ ℝ )
23 22 renegcld ⊢ ( 𝜑 → - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ∈ ℝ )
24 1 5 reipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 , 𝐵 ) ∈ ℝ )
25 14 17 24 syl2anc ⊢ ( 𝜑 → ( 𝐵 , 𝐵 ) ∈ ℝ )
26 2re ⊢ 2 ∈ ℝ
27 readdcl ⊢ ( ( ( 𝐵 , 𝐵 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℝ )
28 25 26 27 sylancl ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℝ )
29 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
30 peano2re ⊢ ( ( 𝐵 , 𝐵 ) ∈ ℝ → ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ℝ )
31 25 30 syl ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ℝ )
32 1 5 ipge0 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ) → 0 ≤ ( 𝐵 , 𝐵 ) )
33 14 17 32 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝐵 , 𝐵 ) )
34 25 ltp1d ⊢ ( 𝜑 → ( 𝐵 , 𝐵 ) < ( ( 𝐵 , 𝐵 ) + 1 ) )
35 29 25 31 33 34 lelttrd ⊢ ( 𝜑 → 0 < ( ( 𝐵 , 𝐵 ) + 1 ) )
36 31 ltp1d ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) < ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) )
37 df-2 ⊢ 2 = ( 1 + 1 )
38 37 oveq2i ⊢ ( ( 𝐵 , 𝐵 ) + 2 ) = ( ( 𝐵 , 𝐵 ) + ( 1 + 1 ) )
39 25 recnd ⊢ ( 𝜑 → ( 𝐵 , 𝐵 ) ∈ ℂ )
40 ax-1cn ⊢ 1 ∈ ℂ
41 addass ⊢ ( ( ( 𝐵 , 𝐵 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) = ( ( 𝐵 , 𝐵 ) + ( 1 + 1 ) ) )
42 40 40 41 mp3an23 ⊢ ( ( 𝐵 , 𝐵 ) ∈ ℂ → ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) = ( ( 𝐵 , 𝐵 ) + ( 1 + 1 ) ) )
43 39 42 syl ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) = ( ( 𝐵 , 𝐵 ) + ( 1 + 1 ) ) )
44 38 43 eqtr4id ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 2 ) = ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) )
45 36 44 breqtrrd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) < ( ( 𝐵 , 𝐵 ) + 2 ) )
46 29 31 28 35 45 lttrd ⊢ ( 𝜑 → 0 < ( ( 𝐵 , 𝐵 ) + 2 ) )
47 28 46 elrpd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℝ+ )
48 oveq2 ⊢ ( 𝑥 = ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) → ( 𝐴 − 𝑥 ) = ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) )
49 48 fveq2d ⊢ ( 𝑥 = ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) → ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) = ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
50 49 breq2d ⊢ ( 𝑥 = ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) → ( ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ↔ ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) )
51 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
52 14 51 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
53 hlphl ⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )
54 7 53 syl ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
55 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
56 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
57 55 5 1 56 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
58 54 9 17 57 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
59 55 56 hlress ⊢ ( 𝑊 ∈ ℂHil → ℝ ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
60 7 59 syl ⊢ ( 𝜑 → ℝ ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
61 60 31 sseldd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
62 25 33 ge0p1rpd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ℝ+ )
63 62 rpne0d ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) ≠ 0 )
64 55 56 cphdivcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( 𝐴 , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝐵 , 𝐵 ) + 1 ) ≠ 0 ) ) → ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
65 14 58 61 63 64 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
66 12 65 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
67 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
68 55 67 56 6 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑈 )
69 52 8 66 10 68 syl22anc ⊢ ( 𝜑 → ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑈 )
70 50 11 69 rspcdva ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
71 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
72 14 71 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
73 1 2 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
74 72 9 73 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
75 1 55 67 56 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐵 ∈ 𝑉 ) → ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 )
76 52 66 17 75 syl3anc ⊢ ( 𝜑 → ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 )
77 1 4 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) → ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 )
78 52 9 76 77 syl3anc ⊢ ( 𝜑 → ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 )
79 1 2 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ∈ ℝ )
80 72 78 79 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ∈ ℝ )
81 1 2 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
82 72 9 81 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
83 1 2 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
84 72 78 83 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
85 74 80 82 84 le2sqd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ≤ ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↔ ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) ) )
86 70 85 mpbid ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) )
87 80 resqcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) ∈ ℝ )
88 74 resqcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
89 87 88 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ) ↔ ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) ) )
90 86 89 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ) )
91 2z ⊢ 2 ∈ ℤ
92 rpexpcl ⊢ ( ( ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ∈ ℝ+ )
93 62 91 92 sylancl ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ∈ ℝ+ )
94 22 93 rerpdivcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) ∈ ℝ )
95 94 28 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ∈ ℝ )
96 95 recnd ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ∈ ℂ )
97 96 negcld ⊢ ( 𝜑 → - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ∈ ℂ )
98 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 , 𝐴 ) ∈ ℂ )
99 14 9 9 98 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐴 ) ∈ ℂ )
100 97 99 pncand ⊢ ( 𝜑 → ( ( - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) + ( 𝐴 , 𝐴 ) ) − ( 𝐴 , 𝐴 ) ) = - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) )
101 1 5 2 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 ) → ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
102 14 78 101 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
103 5 1 4 cphsubdir ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ 𝑉 ) ) → ( ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) )
104 14 9 76 78 103 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) )
105 5 1 4 cphsubdi ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝐴 , 𝐴 ) − ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
106 14 9 9 76 105 syl13anc ⊢ ( 𝜑 → ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝐴 , 𝐴 ) − ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
107 106 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) = ( ( ( 𝐴 , 𝐴 ) − ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) )
108 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ ℂ )
109 14 9 76 108 syl3anc ⊢ ( 𝜑 → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ ℂ )
110 5 1 4 cphsubdi ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) ) → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
111 14 76 9 76 110 syl13anc ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) )
112 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ∈ ℂ )
113 14 76 9 112 syl3anc ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ∈ ℂ )
114 1 5 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ ℂ )
115 14 76 76 114 syl3anc ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ ℂ )
116 113 115 subcld ⊢ ( 𝜑 → ( ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ∈ ℂ )
117 111 116 eqeltrd ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ∈ ℂ )
118 99 109 117 subsub4d ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐴 ) − ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) = ( ( 𝐴 , 𝐴 ) − ( ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) + ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) ) )
119 94 recnd ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) ∈ ℂ )
120 31 recnd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 1 ) ∈ ℂ )
121 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
122 119 120 121 adddid ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) ) = ( ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) + ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · 1 ) ) )
123 44 oveq2d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐵 , 𝐵 ) + 1 ) + 1 ) ) )
124 5 1 55 56 67 cphassr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( ∗ ‘ 𝑇 ) · ( 𝐴 , 𝐵 ) ) )
125 14 66 9 17 124 syl13anc ⊢ ( 𝜑 → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( ∗ ‘ 𝑇 ) · ( 𝐴 , 𝐵 ) ) )
126 19 120 63 divcld ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ∈ ℂ )
127 12 126 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
128 127 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) ∈ ℂ )
129 128 19 mulcomd ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑇 ) · ( 𝐴 , 𝐵 ) ) = ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ 𝑇 ) ) )
130 19 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ∈ ℂ )
131 19 130 120 63 divassd ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( 𝐴 , 𝐵 ) · ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) )
132 19 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) )
133 132 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ ( 𝐴 , 𝐵 ) ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
134 12 fveq2i ⊢ ( ∗ ‘ 𝑇 ) = ( ∗ ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
135 19 120 63 cjdivd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ∗ ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) ) )
136 31 cjred ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( 𝐵 , 𝐵 ) + 1 ) )
137 136 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ∗ ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
138 135 137 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
139 134 138 eqtrid ⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
140 139 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ 𝑇 ) ) = ( ( 𝐴 , 𝐵 ) · ( ( ∗ ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) )
141 131 133 140 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) · ( ∗ ‘ 𝑇 ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
142 125 129 141 3eqtrd ⊢ ( 𝜑 → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
143 22 recnd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ∈ ℂ )
144 143 120 mulcomd ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) )
145 120 sqvald ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) = ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) )
146 144 145 oveq12d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) = ( ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) ) )
147 143 120 120 63 63 divcan5d ⊢ ( 𝜑 → ( ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
148 146 147 eqtr2d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) )
149 93 rpcnd ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ∈ ℂ )
150 93 rpne0d ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ≠ 0 )
151 143 120 149 150 div23d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) )
152 142 148 151 3eqtrd ⊢ ( 𝜑 → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) )
153 94 31 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) ∈ ℝ )
154 152 153 eqeltrd ⊢ ( 𝜑 → ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ∈ ℝ )
155 154 cjred ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) )
156 5 1 cphipcj ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) )
157 14 9 76 156 syl3anc ⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) )
158 155 157 152 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) )
159 5 1 55 56 67 cph2ass ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑇 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐵 , 𝐵 ) ) )
160 14 66 66 17 17 159 syl122anc ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐵 , 𝐵 ) ) )
161 12 fveq2i ⊢ ( abs ‘ 𝑇 ) = ( abs ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
162 19 120 63 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( abs ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) ) )
163 62 rpge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐵 , 𝐵 ) + 1 ) )
164 31 163 absidd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) = ( ( 𝐵 , 𝐵 ) + 1 ) )
165 164 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( abs ‘ ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
166 162 165 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
167 161 166 eqtrid ⊢ ( 𝜑 → ( abs ‘ 𝑇 ) = ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) )
168 167 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ 𝑇 ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ↑ 2 ) )
169 127 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ 𝑇 ) ↑ 2 ) = ( 𝑇 · ( ∗ ‘ 𝑇 ) ) )
170 21 120 63 sqdivd ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) / ( ( 𝐵 , 𝐵 ) + 1 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) )
171 168 169 170 3eqtr3d ⊢ ( 𝜑 → ( 𝑇 · ( ∗ ‘ 𝑇 ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) )
172 171 oveq1d ⊢ ( 𝜑 → ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐵 , 𝐵 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( 𝐵 , 𝐵 ) ) )
173 160 172 eqtrd ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( 𝐵 , 𝐵 ) ) )
174 158 173 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , 𝐴 ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( 𝐵 , 𝐵 ) ) ) )
175 pncan2 ⊢ ( ( ( 𝐵 , 𝐵 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐵 , 𝐵 ) + 1 ) − ( 𝐵 , 𝐵 ) ) = 1 )
176 39 40 175 sylancl ⊢ ( 𝜑 → ( ( ( 𝐵 , 𝐵 ) + 1 ) − ( 𝐵 , 𝐵 ) ) = 1 )
177 176 oveq2d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐵 , 𝐵 ) + 1 ) − ( 𝐵 , 𝐵 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · 1 ) )
178 119 120 39 subdid ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐵 , 𝐵 ) + 1 ) − ( 𝐵 , 𝐵 ) ) ) = ( ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( 𝐵 , 𝐵 ) ) ) )
179 177 178 eqtr3d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · 1 ) = ( ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( 𝐵 , 𝐵 ) ) ) )
180 174 111 179 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · 1 ) )
181 152 180 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) + ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) = ( ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 1 ) ) + ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · 1 ) ) )
182 122 123 181 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) + ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) )
183 182 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) − ( ( 𝐴 , ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) + ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) ) = ( ( 𝐴 , 𝐴 ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) )
184 107 118 183 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) − ( ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) , ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ) = ( ( 𝐴 , 𝐴 ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) )
185 102 104 184 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 , 𝐴 ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) )
186 99 96 negsubd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) + - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) = ( ( 𝐴 , 𝐴 ) − ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) )
187 99 97 addcomd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐴 ) + - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) ) = ( - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) + ( 𝐴 , 𝐴 ) ) )
188 185 186 187 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) = ( - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) + ( 𝐴 , 𝐴 ) ) )
189 1 5 2 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
190 14 9 189 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 , 𝐴 ) )
191 188 190 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ) = ( ( - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) + ( 𝐴 , 𝐴 ) ) − ( 𝐴 , 𝐴 ) ) )
192 28 renegcld ⊢ ( 𝜑 → - ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℝ )
193 192 recnd ⊢ ( 𝜑 → - ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℂ )
194 143 193 149 150 div23d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) )
195 28 recnd ⊢ ( 𝜑 → ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℂ )
196 119 195 mulneg2d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) = - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) )
197 194 196 eqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) = - ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) )
198 100 191 197 3eqtr4rd ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 − ( 𝑇 ( ·𝑠 ‘ 𝑊 ) 𝐵 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) ) )
199 90 198 breqtrrd ⊢ ( 𝜑 → 0 ≤ ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) )
200 22 192 remulcld ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) ∈ ℝ )
201 200 93 ge0divd ⊢ ( 𝜑 → ( 0 ≤ ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) ↔ 0 ≤ ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) / ( ( ( 𝐵 , 𝐵 ) + 1 ) ↑ 2 ) ) ) )
202 199 201 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) )
203 mulneg12 ⊢ ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝐵 , 𝐵 ) + 2 ) ∈ ℂ ) → ( - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) )
204 143 195 203 syl2anc ⊢ ( 𝜑 → ( - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) = ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · - ( ( 𝐵 , 𝐵 ) + 2 ) ) )
205 202 204 breqtrrd ⊢ ( 𝜑 → 0 ≤ ( - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) · ( ( 𝐵 , 𝐵 ) + 2 ) ) )
206 23 47 205 prodge0ld ⊢ ( 𝜑 → 0 ≤ - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) )
207 22 le0neg1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ≤ 0 ↔ 0 ≤ - ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) )
208 206 207 mpbird ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ≤ 0 )
209 20 sqge0d ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) )
210 0re ⊢ 0 ∈ ℝ
211 letri3 ⊢ ( ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) = 0 ↔ ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) ) )
212 22 210 211 sylancl ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) = 0 ↔ ( ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) ) ) )
213 208 209 212 mpbir2and ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 , 𝐵 ) ) ↑ 2 ) = 0 )
214 21 213 sqeq0d ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , 𝐵 ) ) = 0 )
215 19 214 abs00d ⊢ ( 𝜑 → ( 𝐴 , 𝐵 ) = 0 )