This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .+ = ( +g ` W )
cphipfval.s 
|- .x. = ( .s ` W )
cphipfval.n 
|- N = ( norm ` W )
cphipfval.i 
|- ., = ( .i ` W )
cphipval.f 
|- F = ( Scalar ` W )
cphipval.k 
|- K = ( Base ` F )
Assertion cphipval 
|- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A .+ ( ( _i ^ k ) .x. B ) ) ) ^ 2 ) ) / 4 ) )

Proof

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