Metamath Proof Explorer


Theorem cphipval

Description: Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of Ponnusamy p. 361. (Contributed by NM, 31-Jan-2007) (Revised by AV, 18-Oct-2021)

Ref Expression
Hypotheses cphipfval.x X = Base W
cphipfval.p + ˙ = + W
cphipfval.s · ˙ = W
cphipfval.n N = norm W
cphipfval.i , ˙ = 𝑖 W
cphipval.f F = Scalar W
cphipval.k K = Base F
Assertion cphipval W CPreHil i K A X B X A , ˙ B = k = 1 4 i k N A + ˙ i k · ˙ B 2 4

Proof

Step Hyp Ref Expression
1 cphipfval.x X = Base W
2 cphipfval.p + ˙ = + W
3 cphipfval.s · ˙ = W
4 cphipfval.n N = norm W
5 cphipfval.i , ˙ = 𝑖 W
6 cphipval.f F = Scalar W
7 cphipval.k K = Base F
8 eqid - W = - W
9 1 2 3 4 5 8 6 7 cphipval2 W CPreHil i K A X B X A , ˙ B = N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 4
10 ax-icn i
11 10 a1i W CPreHil i K A X B X i
12 simp1l W CPreHil i K A X B X W CPreHil
13 cphngp W CPreHil W NrmGrp
14 ngpgrp W NrmGrp W Grp
15 13 14 syl W CPreHil W Grp
16 15 adantr W CPreHil i K W Grp
17 16 3ad2ant1 W CPreHil i K A X B X W Grp
18 simp2 W CPreHil i K A X B X A X
19 cphlmod W CPreHil W LMod
20 19 3anim1i W CPreHil i K B X W LMod i K B X
21 20 3expa W CPreHil i K B X W LMod i K B X
22 1 6 3 7 lmodvscl W LMod i K B X i · ˙ B X
23 21 22 syl W CPreHil i K B X i · ˙ B X
24 23 3adant2 W CPreHil i K A X B X i · ˙ B X
25 1 2 grpcl W Grp A X i · ˙ B X A + ˙ i · ˙ B X
26 17 18 24 25 syl3anc W CPreHil i K A X B X A + ˙ i · ˙ B X
27 1 5 4 nmsq W CPreHil A + ˙ i · ˙ B X N A + ˙ i · ˙ B 2 = A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
28 12 26 27 syl2anc W CPreHil i K A X B X N A + ˙ i · ˙ B 2 = A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
29 1 5 reipcl W CPreHil A + ˙ i · ˙ B X A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
30 12 26 29 syl2anc W CPreHil i K A X B X A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
31 30 recnd W CPreHil i K A X B X A + ˙ i · ˙ B , ˙ A + ˙ i · ˙ B
32 28 31 eqeltrd W CPreHil i K A X B X N A + ˙ i · ˙ B 2
33 11 32 mulcld W CPreHil i K A X B X i N A + ˙ i · ˙ B 2
34 19 adantr W CPreHil i K W LMod
35 34 3ad2ant1 W CPreHil i K A X B X W LMod
36 cphclm W CPreHil W CMod
37 6 7 clmneg1 W CMod 1 K
38 36 37 syl W CPreHil 1 K
39 38 adantr W CPreHil i K 1 K
40 39 3ad2ant1 W CPreHil i K A X B X 1 K
41 simp3 W CPreHil i K A X B X B X
42 1 6 3 7 lmodvscl W LMod 1 K B X -1 · ˙ B X
43 35 40 41 42 syl3anc W CPreHil i K A X B X -1 · ˙ B X
44 1 2 grpcl W Grp A X -1 · ˙ B X A + ˙ -1 · ˙ B X
45 17 18 43 44 syl3anc W CPreHil i K A X B X A + ˙ -1 · ˙ B X
46 1 5 4 nmsq W CPreHil A + ˙ -1 · ˙ B X N A + ˙ -1 · ˙ B 2 = A + ˙ -1 · ˙ B , ˙ A + ˙ -1 · ˙ B
47 12 45 46 syl2anc W CPreHil i K A X B X N A + ˙ -1 · ˙ B 2 = A + ˙ -1 · ˙ B , ˙ A + ˙ -1 · ˙ B
48 1 5 reipcl W CPreHil A + ˙ -1 · ˙ B X A + ˙ -1 · ˙ B , ˙ A + ˙ -1 · ˙ B
49 12 45 48 syl2anc W CPreHil i K A X B X A + ˙ -1 · ˙ B , ˙ A + ˙ -1 · ˙ B
50 47 49 eqeltrd W CPreHil i K A X B X N A + ˙ -1 · ˙ B 2
51 50 recnd W CPreHil i K A X B X N A + ˙ -1 · ˙ B 2
52 addneg1mul i N A + ˙ i · ˙ B 2 N A + ˙ -1 · ˙ B 2 i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A + ˙ -1 · ˙ B 2
53 33 51 52 syl2anc W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A + ˙ -1 · ˙ B 2
54 36 adantr W CPreHil i K W CMod
55 1 2 8 6 3 clmvsubval W CMod A X B X A - W B = A + ˙ -1 · ˙ B
56 55 eqcomd W CMod A X B X A + ˙ -1 · ˙ B = A - W B
57 54 56 syl3an1 W CPreHil i K A X B X A + ˙ -1 · ˙ B = A - W B
58 57 fveq2d W CPreHil i K A X B X N A + ˙ -1 · ˙ B = N A - W B
59 58 oveq1d W CPreHil i K A X B X N A + ˙ -1 · ˙ B 2 = N A - W B 2
60 59 oveq2d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A + ˙ -1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2
61 53 60 eqtrd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2
62 eqid inv g W = inv g W
63 54 3ad2ant1 W CPreHil i K A X B X W CMod
64 simp1r W CPreHil i K A X B X i K
65 1 6 3 62 7 63 41 64 clmvsneg W CPreHil i K A X B X inv g W i · ˙ B = i · ˙ B
66 65 eqcomd W CPreHil i K A X B X i · ˙ B = inv g W i · ˙ B
67 66 oveq2d W CPreHil i K A X B X A + ˙ i · ˙ B = A + ˙ inv g W i · ˙ B
68 1 2 62 8 grpsubval A X i · ˙ B X A - W i · ˙ B = A + ˙ inv g W i · ˙ B
69 18 24 68 syl2anc W CPreHil i K A X B X A - W i · ˙ B = A + ˙ inv g W i · ˙ B
70 67 69 eqtr4d W CPreHil i K A X B X A + ˙ i · ˙ B = A - W i · ˙ B
71 70 fveq2d W CPreHil i K A X B X N A + ˙ i · ˙ B = N A - W i · ˙ B
72 71 oveq1d W CPreHil i K A X B X N A + ˙ i · ˙ B 2 = N A - W i · ˙ B 2
73 72 oveq2d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 = i N A - W i · ˙ B 2
74 61 73 oveq12d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 + i N A - W i · ˙ B 2
75 54 anim1i W CPreHil i K B X W CMod B X
76 75 3adant2 W CPreHil i K A X B X W CMod B X
77 1 3 clmvs1 W CMod B X 1 · ˙ B = B
78 76 77 syl W CPreHil i K A X B X 1 · ˙ B = B
79 78 oveq2d W CPreHil i K A X B X A + ˙ 1 · ˙ B = A + ˙ B
80 79 fveq2d W CPreHil i K A X B X N A + ˙ 1 · ˙ B = N A + ˙ B
81 80 oveq1d W CPreHil i K A X B X N A + ˙ 1 · ˙ B 2 = N A + ˙ B 2
82 81 oveq2d W CPreHil i K A X B X 1 N A + ˙ 1 · ˙ B 2 = 1 N A + ˙ B 2
83 1 2 grpcl W Grp A X B X A + ˙ B X
84 16 83 syl3an1 W CPreHil i K A X B X A + ˙ B X
85 1 5 4 nmsq W CPreHil A + ˙ B X N A + ˙ B 2 = A + ˙ B , ˙ A + ˙ B
86 12 84 85 syl2anc W CPreHil i K A X B X N A + ˙ B 2 = A + ˙ B , ˙ A + ˙ B
87 1 5 reipcl W CPreHil A + ˙ B X A + ˙ B , ˙ A + ˙ B
88 12 84 87 syl2anc W CPreHil i K A X B X A + ˙ B , ˙ A + ˙ B
89 86 88 eqeltrd W CPreHil i K A X B X N A + ˙ B 2
90 89 recnd W CPreHil i K A X B X N A + ˙ B 2
91 90 mulid2d W CPreHil i K A X B X 1 N A + ˙ B 2 = N A + ˙ B 2
92 82 91 eqtrd W CPreHil i K A X B X 1 N A + ˙ 1 · ˙ B 2 = N A + ˙ B 2
93 74 92 oveq12d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 + 1 N A + ˙ 1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2 + i N A - W i · ˙ B 2 + N A + ˙ B 2
94 nnuz = 1
95 df-4 4 = 3 + 1
96 oveq2 k = 4 i k = i 4
97 i4 i 4 = 1
98 96 97 eqtrdi k = 4 i k = 1
99 98 oveq1d k = 4 i k · ˙ B = 1 · ˙ B
100 99 oveq2d k = 4 A + ˙ i k · ˙ B = A + ˙ 1 · ˙ B
101 100 fveq2d k = 4 N A + ˙ i k · ˙ B = N A + ˙ 1 · ˙ B
102 101 oveq1d k = 4 N A + ˙ i k · ˙ B 2 = N A + ˙ 1 · ˙ B 2
103 98 102 oveq12d k = 4 i k N A + ˙ i k · ˙ B 2 = 1 N A + ˙ 1 · ˙ B 2
104 10 a1i k i
105 nnnn0 k k 0
106 104 105 expcld k i k
107 106 adantl W CPreHil i K A X B X k i k
108 12 adantr W CPreHil i K A X B X k W CPreHil
109 17 adantr W CPreHil i K A X B X k W Grp
110 18 adantr W CPreHil i K A X B X k A X
111 35 adantr W CPreHil i K A X B X k W LMod
112 36 anim1i W CPreHil i K W CMod i K
113 112 3ad2ant1 W CPreHil i K A X B X W CMod i K
114 6 7 cmodscexp W CMod i K k i k K
115 113 114 sylan W CPreHil i K A X B X k i k K
116 41 adantr W CPreHil i K A X B X k B X
117 1 6 3 7 lmodvscl W LMod i k K B X i k · ˙ B X
118 111 115 116 117 syl3anc W CPreHil i K A X B X k i k · ˙ B X
119 1 2 grpcl W Grp A X i k · ˙ B X A + ˙ i k · ˙ B X
120 109 110 118 119 syl3anc W CPreHil i K A X B X k A + ˙ i k · ˙ B X
121 1 5 4 nmsq W CPreHil A + ˙ i k · ˙ B X N A + ˙ i k · ˙ B 2 = A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
122 108 120 121 syl2anc W CPreHil i K A X B X k N A + ˙ i k · ˙ B 2 = A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
123 1 5 reipcl W CPreHil A + ˙ i k · ˙ B X A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
124 108 120 123 syl2anc W CPreHil i K A X B X k A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
125 124 recnd W CPreHil i K A X B X k A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
126 122 125 eqeltrd W CPreHil i K A X B X k N A + ˙ i k · ˙ B 2
127 107 126 mulcld W CPreHil i K A X B X k i k N A + ˙ i k · ˙ B 2
128 df-3 3 = 2 + 1
129 oveq2 k = 3 i k = i 3
130 i3 i 3 = i
131 129 130 eqtrdi k = 3 i k = i
132 131 oveq1d k = 3 i k · ˙ B = i · ˙ B
133 132 oveq2d k = 3 A + ˙ i k · ˙ B = A + ˙ i · ˙ B
134 133 fveq2d k = 3 N A + ˙ i k · ˙ B = N A + ˙ i · ˙ B
135 134 oveq1d k = 3 N A + ˙ i k · ˙ B 2 = N A + ˙ i · ˙ B 2
136 131 135 oveq12d k = 3 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2
137 10 a1i W CPreHil i K A X B X k i
138 105 adantl W CPreHil i K A X B X k k 0
139 137 138 expcld W CPreHil i K A X B X k i k
140 123 recnd W CPreHil A + ˙ i k · ˙ B X A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
141 108 120 140 syl2anc W CPreHil i K A X B X k A + ˙ i k · ˙ B , ˙ A + ˙ i k · ˙ B
142 122 141 eqeltrd W CPreHil i K A X B X k N A + ˙ i k · ˙ B 2
143 139 142 mulcld W CPreHil i K A X B X k i k N A + ˙ i k · ˙ B 2
144 df-2 2 = 1 + 1
145 oveq2 k = 2 i k = i 2
146 i2 i 2 = 1
147 145 146 eqtrdi k = 2 i k = 1
148 147 oveq1d k = 2 i k · ˙ B = -1 · ˙ B
149 148 oveq2d k = 2 A + ˙ i k · ˙ B = A + ˙ -1 · ˙ B
150 149 fveq2d k = 2 N A + ˙ i k · ˙ B = N A + ˙ -1 · ˙ B
151 150 oveq1d k = 2 N A + ˙ i k · ˙ B 2 = N A + ˙ -1 · ˙ B 2
152 147 151 oveq12d k = 2 i k N A + ˙ i k · ˙ B 2 = -1 N A + ˙ -1 · ˙ B 2
153 139 126 mulcld W CPreHil i K A X B X k i k N A + ˙ i k · ˙ B 2
154 1z 1
155 oveq2 k = 1 i k = i 1
156 exp1 i i 1 = i
157 10 156 ax-mp i 1 = i
158 155 157 eqtrdi k = 1 i k = i
159 158 oveq1d k = 1 i k · ˙ B = i · ˙ B
160 159 oveq2d k = 1 A + ˙ i k · ˙ B = A + ˙ i · ˙ B
161 160 fveq2d k = 1 N A + ˙ i k · ˙ B = N A + ˙ i · ˙ B
162 161 oveq1d k = 1 N A + ˙ i k · ˙ B 2 = N A + ˙ i · ˙ B 2
163 158 162 oveq12d k = 1 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2
164 163 fsum1 1 i N A + ˙ i · ˙ B 2 k = 1 1 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2
165 154 33 164 sylancr W CPreHil i K A X B X k = 1 1 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2
166 1nn 1
167 165 166 jctil W CPreHil i K A X B X 1 k = 1 1 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2
168 eqidd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2
169 94 144 152 153 167 168 fsump1i W CPreHil i K A X B X 2 k = 1 2 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2
170 eqidd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2
171 94 128 136 143 169 170 fsump1i W CPreHil i K A X B X 3 k = 1 3 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2
172 eqidd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 + 1 N A + ˙ 1 · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 + 1 N A + ˙ 1 · ˙ B 2
173 94 95 103 127 171 172 fsump1i W CPreHil i K A X B X 4 k = 1 4 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 + 1 N A + ˙ 1 · ˙ B 2
174 173 simprd W CPreHil i K A X B X k = 1 4 i k N A + ˙ i k · ˙ B 2 = i N A + ˙ i · ˙ B 2 + -1 N A + ˙ -1 · ˙ B 2 + i N A + ˙ i · ˙ B 2 + 1 N A + ˙ 1 · ˙ B 2
175 1 8 grpsubcl W Grp A X B X A - W B X
176 16 175 syl3an1 W CPreHil i K A X B X A - W B X
177 1 5 4 nmsq W CPreHil A - W B X N A - W B 2 = A - W B , ˙ A - W B
178 12 176 177 syl2anc W CPreHil i K A X B X N A - W B 2 = A - W B , ˙ A - W B
179 1 5 reipcl W CPreHil A - W B X A - W B , ˙ A - W B
180 12 176 179 syl2anc W CPreHil i K A X B X A - W B , ˙ A - W B
181 178 180 eqeltrd W CPreHil i K A X B X N A - W B 2
182 181 recnd W CPreHil i K A X B X N A - W B 2
183 90 182 subcld W CPreHil i K A X B X N A + ˙ B 2 N A - W B 2
184 1 8 grpsubcl W Grp A X i · ˙ B X A - W i · ˙ B X
185 17 18 24 184 syl3anc W CPreHil i K A X B X A - W i · ˙ B X
186 1 5 4 nmsq W CPreHil A - W i · ˙ B X N A - W i · ˙ B 2 = A - W i · ˙ B , ˙ A - W i · ˙ B
187 12 185 186 syl2anc W CPreHil i K A X B X N A - W i · ˙ B 2 = A - W i · ˙ B , ˙ A - W i · ˙ B
188 1 5 reipcl W CPreHil A - W i · ˙ B X A - W i · ˙ B , ˙ A - W i · ˙ B
189 12 185 188 syl2anc W CPreHil i K A X B X A - W i · ˙ B , ˙ A - W i · ˙ B
190 187 189 eqeltrd W CPreHil i K A X B X N A - W i · ˙ B 2
191 190 recnd W CPreHil i K A X B X N A - W i · ˙ B 2
192 32 191 subcld W CPreHil i K A X B X N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2
193 11 192 mulcld W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2
194 183 193 addcomd W CPreHil i K A X B X N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 + N A + ˙ B 2 - N A - W B 2
195 193 182 90 subadd23d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 - N A - W B 2 + N A + ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 + N A + ˙ B 2 - N A - W B 2
196 11 32 191 subdid W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 i N A - W i · ˙ B 2
197 196 oveq1d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 N A - W B 2 = i N A + ˙ i · ˙ B 2 - i N A - W i · ˙ B 2 - N A - W B 2
198 11 191 mulcld W CPreHil i K A X B X i N A - W i · ˙ B 2
199 33 198 182 sub32d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 - i N A - W i · ˙ B 2 - N A - W B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 - i N A - W i · ˙ B 2
200 197 199 eqtrd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 N A - W B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 - i N A - W i · ˙ B 2
201 200 oveq1d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 - N A - W B 2 + N A + ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2 - i N A - W i · ˙ B 2 + N A + ˙ B 2
202 194 195 201 3eqtr2d W CPreHil i K A X B X N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2 - i N A - W i · ˙ B 2 + N A + ˙ B 2
203 33 182 subcld W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W B 2
204 203 198 negsubd W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 - N A - W B 2 + i N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 - i N A - W i · ˙ B 2
205 11 191 mulneg1d W CPreHil i K A X B X i N A - W i · ˙ B 2 = i N A - W i · ˙ B 2
206 205 eqcomd W CPreHil i K A X B X i N A - W i · ˙ B 2 = i N A - W i · ˙ B 2
207 206 oveq2d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 - N A - W B 2 + i N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 + i N A - W i · ˙ B 2
208 204 207 eqtr3d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 - N A - W B 2 - i N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 - N A - W B 2 + i N A - W i · ˙ B 2
209 208 oveq1d W CPreHil i K A X B X i N A + ˙ i · ˙ B 2 N A - W B 2 - i N A - W i · ˙ B 2 + N A + ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2 + i N A - W i · ˙ B 2 + N A + ˙ B 2
210 202 209 eqtrd W CPreHil i K A X B X N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 = i N A + ˙ i · ˙ B 2 N A - W B 2 + i N A - W i · ˙ B 2 + N A + ˙ B 2
211 93 174 210 3eqtr4rd W CPreHil i K A X B X N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 = k = 1 4 i k N A + ˙ i k · ˙ B 2
212 211 oveq1d W CPreHil i K A X B X N A + ˙ B 2 - N A - W B 2 + i N A + ˙ i · ˙ B 2 N A - W i · ˙ B 2 4 = k = 1 4 i k N A + ˙ i k · ˙ B 2 4
213 9 212 eqtrd W CPreHil i K A X B X A , ˙ B = k = 1 4 i k N A + ˙ i k · ˙ B 2 4