Step |
Hyp |
Ref |
Expression |
1 |
|
simpl2l |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) ) |
2 |
|
fveecn |
|- ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC ) |
3 |
1 2
|
sylancom |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
4 |
|
simpl2r |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) ) |
5 |
|
fveecn |
|- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC ) |
6 |
4 5
|
sylancom |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
7 |
|
elicc01 |
|- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) ) |
8 |
7
|
simp1bi |
|- ( T e. ( 0 [,] 1 ) -> T e. RR ) |
9 |
8
|
recnd |
|- ( T e. ( 0 [,] 1 ) -> T e. CC ) |
10 |
9
|
adantr |
|- ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> T e. CC ) |
11 |
10
|
3ad2ant3 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
12 |
11
|
adantr |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
13 |
|
fveq2 |
|- ( i = j -> ( B ` i ) = ( B ` j ) ) |
14 |
|
fveq2 |
|- ( i = j -> ( A ` i ) = ( A ` j ) ) |
15 |
14
|
oveq2d |
|- ( i = j -> ( ( 1 - T ) x. ( A ` i ) ) = ( ( 1 - T ) x. ( A ` j ) ) ) |
16 |
|
fveq2 |
|- ( i = j -> ( C ` i ) = ( C ` j ) ) |
17 |
16
|
oveq2d |
|- ( i = j -> ( T x. ( C ` i ) ) = ( T x. ( C ` j ) ) ) |
18 |
15 17
|
oveq12d |
|- ( i = j -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) |
19 |
13 18
|
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 ) ) ) ) ) |
20 |
19
|
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 ) ) ) ) |
21 |
20
|
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 ) ) ) ) |
22 |
21
|
3ad2antl3 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) ) ) ) |
23 |
|
oveq1 |
|- ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( B ` j ) - ( C ` j ) ) = ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ) |
24 |
23
|
oveq1d |
|- ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) ) |
25 |
|
ax-1cn |
|- 1 e. CC |
26 |
|
subcl |
|- ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC ) |
27 |
25 26
|
mpan |
|- ( T e. CC -> ( 1 - T ) e. CC ) |
28 |
27
|
3ad2ant3 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( 1 - T ) e. CC ) |
29 |
|
simp1 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( A ` j ) e. CC ) |
30 |
28 29
|
mulcld |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC ) |
31 |
|
simp3 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> T e. CC ) |
32 |
|
simp2 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( C ` j ) e. CC ) |
33 |
31 32
|
mulcld |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( T x. ( C ` j ) ) e. CC ) |
34 |
30 33 32
|
addsubassd |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) ) |
35 |
|
subdi |
|- ( ( ( 1 - T ) e. CC /\ ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) ) |
36 |
27 35
|
syl3an1 |
|- ( ( T e. CC /\ ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) ) |
37 |
36
|
3coml |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) ) |
38 |
|
subdir |
|- ( ( 1 e. CC /\ T e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) ) |
39 |
25 38
|
mp3an1 |
|- ( ( T e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) ) |
40 |
39
|
ancoms |
|- ( ( ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) ) |
41 |
40
|
3adant1 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) ) |
42 |
|
mulid2 |
|- ( ( C ` j ) e. CC -> ( 1 x. ( C ` j ) ) = ( C ` j ) ) |
43 |
42
|
oveq1d |
|- ( ( C ` j ) e. CC -> ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) |
44 |
43
|
3ad2ant2 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) |
45 |
41 44
|
eqtrd |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) |
46 |
45
|
oveq2d |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) ) |
47 |
30 32 33
|
subsub2d |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) ) |
48 |
37 46 47
|
3eqtrd |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) ) |
49 |
34 48
|
eqtr4d |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) = ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) ) |
50 |
49
|
oveq1d |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) ) |
51 |
|
subcl |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC ) |
52 |
51
|
3adant3 |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC ) |
53 |
28 52
|
sqmuld |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
54 |
50 53
|
eqtrd |
|- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
55 |
24 54
|
sylan9eqr |
|- ( ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) /\ ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) -> ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
56 |
3 6 12 22 55
|
syl31anc |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
57 |
56
|
sumeq2dv |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
58 |
|
fzfid |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
59 |
|
1re |
|- 1 e. RR |
60 |
|
resubcl |
|- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR ) |
61 |
59 8 60
|
sylancr |
|- ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. RR ) |
62 |
61
|
resqcld |
|- ( T e. ( 0 [,] 1 ) -> ( ( 1 - T ) ^ 2 ) e. RR ) |
63 |
62
|
recnd |
|- ( T e. ( 0 [,] 1 ) -> ( ( 1 - T ) ^ 2 ) e. CC ) |
64 |
63
|
adantr |
|- ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( ( 1 - T ) ^ 2 ) e. CC ) |
65 |
64
|
3ad2ant3 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) ^ 2 ) e. CC ) |
66 |
2
|
3adant1 |
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC ) |
67 |
66
|
3adant2r |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC ) |
68 |
5
|
3adant1 |
|- ( ( N e. NN /\ C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC ) |
69 |
68
|
3adant2l |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC ) |
70 |
67 69
|
subcld |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. CC ) |
71 |
70
|
sqcld |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC ) |
72 |
71
|
3expa |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC ) |
73 |
72
|
3adantl3 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) |
74 |
58 65 73
|
fsummulc2 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |
75 |
57 74
|
eqtr4d |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C 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 ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) ) |