Metamath Proof Explorer

Theorem ipval2

Description: Expansion of the inner product value ipval . (Contributed by NM, 31-Jan-2007) (Revised by Mario Carneiro, 5-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 
|- X = ( BaseSet ` U )
dipfval.2 
|- G = ( +v ` U )
dipfval.4 
|- S = ( .sOLD ` U )
dipfval.6 
|- N = ( normCV ` U )
dipfval.7 
|- P = ( .iOLD ` U )
Assertion ipval2 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 dipfval.1 
 |-  X = ( BaseSet ` U )
2 dipfval.2 
 |-  G = ( +v ` U )
3 dipfval.4 
 |-  S = ( .sOLD ` U )
4 dipfval.6 
 |-  N = ( normCV ` U )
5 dipfval.7 
 |-  P = ( .iOLD ` U )
6 1 2 3 4 5 ipval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) / 4 ) )
7 ax-icn 
 |-  _i e. CC
8 1 2 3 4 5 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ _i e. CC ) -> ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC )
9 7 8 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC )
10 mulcl 
 |-  ( ( _i e. CC /\ ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC ) -> ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) e. CC )
11 7 9 10 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) e. CC )
12 neg1cn 
 |-  -u 1 e. CC
13 1 2 3 4 5 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u 1 e. CC ) -> ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) e. CC )
14 12 13 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) e. CC )
15 11 14 subcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) e. CC )
16 negicn 
 |-  -u _i e. CC
17 1 2 3 4 5 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ -u _i e. CC ) -> ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC )
18 16 17 mpan2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC )
19 mulcl 
 |-  ( ( _i e. CC /\ ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC ) -> ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC )
20 7 18 19 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC )
21 15 20 negsubd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + -u ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
22 14 mulm1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = -u ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) )
23 22 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + -u ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
24 11 14 negsubd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + -u ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
25 23 24 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
26 mulneg1 
 |-  ( ( _i e. CC /\ ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC ) -> ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) = -u ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) )
27 7 18 26 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) = -u ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) )
28 25 27 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + -u ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
29 subdi 
 |-  ( ( _i e. CC /\ ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC /\ ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
30 7 29 mp3an1 
 |-  ( ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC /\ ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
31 9 18 30 syl2anc 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
32 31 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
33 11 20 14 sub32d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
34 32 33 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) - ( _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
35 21 28 34 3eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
36 1 3 nvsid 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( 1 S B ) = B )
37 36 oveq2d 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( A G ( 1 S B ) ) = ( A G B ) )
38 37 fveq2d 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` ( A G ( 1 S B ) ) ) = ( N ` ( A G B ) ) )
39 38 oveq1d 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
40 39 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) = ( ( N ` ( A G B ) ) ^ 2 ) )
41 40 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) = ( 1 x. ( ( N ` ( A G B ) ) ^ 2 ) ) )
42 1 2 3 4 5 ipval2lem3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. RR )
43 42 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. CC )
44 43 mullidd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 1 x. ( ( N ` ( A G B ) ) ^ 2 ) ) = ( ( N ` ( A G B ) ) ^ 2 ) )
45 41 44 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) = ( ( N ` ( A G B ) ) ^ 2 ) )
46 35 45 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) ) = ( ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( ( N ` ( A G B ) ) ^ 2 ) ) )
47 nnuz 
 |-  NN = ( ZZ>= ` 1 )
48 df-4 
 |-  4 = ( 3 + 1 )
49 oveq2 
 |-  ( k = 4 -> ( _i ^ k ) = ( _i ^ 4 ) )
50 i4 
 |-  ( _i ^ 4 ) = 1
51 49 50 eqtrdi 
 |-  ( k = 4 -> ( _i ^ k ) = 1 )
52 51 oveq1d 
 |-  ( k = 4 -> ( ( _i ^ k ) S B ) = ( 1 S B ) )
53 52 oveq2d 
 |-  ( k = 4 -> ( A G ( ( _i ^ k ) S B ) ) = ( A G ( 1 S B ) ) )
54 53 fveq2d 
 |-  ( k = 4 -> ( N ` ( A G ( ( _i ^ k ) S B ) ) ) = ( N ` ( A G ( 1 S B ) ) ) )
55 54 oveq1d 
 |-  ( k = 4 -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) = ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) )
56 51 55 oveq12d 
 |-  ( k = 4 -> ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) )
57 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
58 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
59 7 57 58 sylancr 
 |-  ( k e. NN -> ( _i ^ k ) e. CC )
60 59 adantl 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. NN ) -> ( _i ^ k ) e. CC )
61 1 2 3 4 5 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ ( _i ^ k ) e. CC ) -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) e. CC )
62 59 61 sylan2 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. NN ) -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) e. CC )
63 60 62 mulcld 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. NN ) -> ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) e. CC )
64 df-3 
 |-  3 = ( 2 + 1 )
65 oveq2 
 |-  ( k = 3 -> ( _i ^ k ) = ( _i ^ 3 ) )
66 i3 
 |-  ( _i ^ 3 ) = -u _i
67 65 66 eqtrdi 
 |-  ( k = 3 -> ( _i ^ k ) = -u _i )
68 67 oveq1d 
 |-  ( k = 3 -> ( ( _i ^ k ) S B ) = ( -u _i S B ) )
69 68 oveq2d 
 |-  ( k = 3 -> ( A G ( ( _i ^ k ) S B ) ) = ( A G ( -u _i S B ) ) )
70 69 fveq2d 
 |-  ( k = 3 -> ( N ` ( A G ( ( _i ^ k ) S B ) ) ) = ( N ` ( A G ( -u _i S B ) ) ) )
71 70 oveq1d 
 |-  ( k = 3 -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) = ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) )
72 67 71 oveq12d 
 |-  ( k = 3 -> ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) )
73 df-2 
 |-  2 = ( 1 + 1 )
74 oveq2 
 |-  ( k = 2 -> ( _i ^ k ) = ( _i ^ 2 ) )
75 i2 
 |-  ( _i ^ 2 ) = -u 1
76 74 75 eqtrdi 
 |-  ( k = 2 -> ( _i ^ k ) = -u 1 )
77 76 oveq1d 
 |-  ( k = 2 -> ( ( _i ^ k ) S B ) = ( -u 1 S B ) )
78 77 oveq2d 
 |-  ( k = 2 -> ( A G ( ( _i ^ k ) S B ) ) = ( A G ( -u 1 S B ) ) )
79 78 fveq2d 
 |-  ( k = 2 -> ( N ` ( A G ( ( _i ^ k ) S B ) ) ) = ( N ` ( A G ( -u 1 S B ) ) ) )
80 79 oveq1d 
 |-  ( k = 2 -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) = ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) )
81 76 80 oveq12d 
 |-  ( k = 2 -> ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
82 1z 
 |-  1 e. ZZ
83 oveq2 
 |-  ( k = 1 -> ( _i ^ k ) = ( _i ^ 1 ) )
84 exp1 
 |-  ( _i e. CC -> ( _i ^ 1 ) = _i )
85 7 84 ax-mp 
 |-  ( _i ^ 1 ) = _i
86 83 85 eqtrdi 
 |-  ( k = 1 -> ( _i ^ k ) = _i )
87 86 oveq1d 
 |-  ( k = 1 -> ( ( _i ^ k ) S B ) = ( _i S B ) )
88 87 oveq2d 
 |-  ( k = 1 -> ( A G ( ( _i ^ k ) S B ) ) = ( A G ( _i S B ) ) )
89 88 fveq2d 
 |-  ( k = 1 -> ( N ` ( A G ( ( _i ^ k ) S B ) ) ) = ( N ` ( A G ( _i S B ) ) ) )
90 89 oveq1d 
 |-  ( k = 1 -> ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) = ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) )
91 86 90 oveq12d 
 |-  ( k = 1 -> ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) )
92 91 fsum1 
 |-  ( ( 1 e. ZZ /\ ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) e. CC ) -> sum_ k e. ( 1 ... 1 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) )
93 82 11 92 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> sum_ k e. ( 1 ... 1 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) )
94 1nn 
 |-  1 e. NN
95 93 94 jctil 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 1 e. NN /\ sum_ k e. ( 1 ... 1 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) ) )
96 eqidd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) )
97 47 73 81 63 95 96 fsump1i 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 2 e. NN /\ sum_ k e. ( 1 ... 2 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) ) )
98 eqidd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
99 47 64 72 63 97 98 fsump1i 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 3 e. NN /\ sum_ k e. ( 1 ... 3 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) )
100 eqidd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) ) = ( ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) ) )
101 47 48 56 63 99 100 fsump1i 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 e. NN /\ sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) ) ) )
102 101 simprd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( ( ( ( _i x. ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) ) + ( -u 1 x. ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) + ( -u _i x. ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( 1 x. ( ( N ` ( A G ( 1 S B ) ) ) ^ 2 ) ) ) )
103 43 14 subcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) e. CC )
104 9 18 subcld 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC )
105 mulcl 
 |-  ( ( _i e. CC /\ ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) e. CC )
106 7 104 105 sylancr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) e. CC )
107 103 106 addcomd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) = ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) )
108 106 14 43 subadd23d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( ( N ` ( A G B ) ) ^ 2 ) ) = ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) + ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) ) )
109 107 108 eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) = ( ( ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( ( N ` ( A G B ) ) ^ 2 ) ) )
110 46 102 109 3eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) = ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) )
111 110 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A G ( ( _i ^ k ) S B ) ) ) ^ 2 ) ) / 4 ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )
112 6 111 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )