Metamath Proof Explorer

Theorem ax5seglem9

Description: Lemma for ax5seg . Take the calculation in ax5seglem8 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion ax5seglem9 
|- ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( T x. sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simprll 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> A e. ( EE ` N ) )
2 1 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
3 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
4 2 3 sylancom 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
5 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
6 5 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
7 6 recnd 
 |-  ( T e. ( 0 [,] 1 ) -> T e. CC )
8 7 ad2antrl 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> T e. CC )
9 8 adantr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> T e. CC )
10 simprrl 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> C e. ( EE ` N ) )
11 10 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
12 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
13 11 12 sylancom 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
14 simprrr 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> D e. ( EE ` N ) )
15 14 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> D e. ( EE ` N ) )
16 fveecn 
 |-  ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. CC )
17 15 16 sylancom 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. CC )
18 fveq2 
 |-  ( i = j -> ( B ` i ) = ( B ` j ) )
19 fveq2 
 |-  ( i = j -> ( A ` i ) = ( A ` j ) )
20 19 oveq2d 
 |-  ( i = j -> ( ( 1 - T ) x. ( A ` i ) ) = ( ( 1 - T ) x. ( A ` j ) ) )
21 fveq2 
 |-  ( i = j -> ( C ` i ) = ( C ` j ) )
22 21 oveq2d 
 |-  ( i = j -> ( T x. ( C ` i ) ) = ( T x. ( C ` j ) ) )
23 20 22 oveq12d 
 |-  ( i = j -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
24 18 23 eqeq12d 
 |-  ( i = j -> ( ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) <-> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) )
25 24 rspccva 
 |-  ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
26 25 adantll 
 |-  ( ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
27 26 adantll 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
28 ax5seglem8 
 |-  ( ( ( ( A ` j ) e. CC /\ T e. CC ) /\ ( ( C ` j ) e. CC /\ ( D ` j ) e. CC ) ) -> ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
29 oveq1 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( B ` j ) - ( D ` j ) ) = ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( D ` j ) ) )
30 29 oveq1d 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) = ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( D ` j ) ) ^ 2 ) )
31 30 oveq1d 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = ( ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
32 31 eqcomd 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
33 28 32 sylan9eq 
 |-  ( ( ( ( ( A ` j ) e. CC /\ T e. CC ) /\ ( ( C ` j ) e. CC /\ ( D ` j ) e. CC ) ) /\ ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) -> ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
34 33 3impa 
 |-  ( ( ( ( A ` j ) e. CC /\ T e. CC ) /\ ( ( C ` j ) e. CC /\ ( D ` j ) e. CC ) /\ ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) -> ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
35 4 9 13 17 27 34 syl221anc 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
36 35 sumeq2dv 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
37 fzfid 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( 1 ... N ) e. Fin )
38 13 17 subcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( C ` j ) - ( D ` j ) ) e. CC )
39 38 sqcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. CC )
40 37 8 39 fsummulc2 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( T x. sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( T x. ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) )
41 4 13 subcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
42 41 sqcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
43 37 8 42 fsummulc2 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
44 43 oveq1d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) )
45 9 42 mulcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) e. CC )
46 4 17 subcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( D ` j ) ) e. CC )
47 46 sqcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) e. CC )
48 37 45 47 fsumsub 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) )
49 44 48 eqtr4d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) )
50 49 oveq2d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) = ( ( 1 - T ) x. sum_ j e. ( 1 ... N ) ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) )
51 ax-1cn 
 |-  1 e. CC
52 subcl 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
53 51 8 52 sylancr 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( 1 - T ) e. CC )
54 45 47 subcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) e. CC )
55 37 53 54 fsummulc2 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( 1 - T ) x. sum_ j e. ( 1 ... N ) ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) = sum_ j e. ( 1 ... N ) ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) )
56 50 55 eqtrd 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) = sum_ j e. ( 1 ... N ) ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) )
57 56 oveq2d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + sum_ j e. ( 1 ... N ) ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
58 simprlr 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> B e. ( EE ` N ) )
59 58 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> B e. ( EE ` N ) )
60 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) e. CC )
61 59 60 sylancom 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) e. CC )
62 61 17 subcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( B ` j ) - ( D ` j ) ) e. CC )
63 62 sqcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) e. CC )
64 51 9 52 sylancr 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( 1 - T ) e. CC )
65 64 54 mulcld 
 |-  ( ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) e. CC )
66 37 63 65 fsumadd 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + sum_ j e. ( 1 ... N ) ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
67 57 66 eqtr4d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = sum_ j e. ( 1 ... N ) ( ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
68 36 40 67 3eqtr4d 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( T x. sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - T ) x. ( ( T x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )