Metamath Proof Explorer

Theorem ax5seglem1

Description: Lemma for ax5seg . Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem1 
|- ( ( 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 ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )

Proof

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 adantr 
 |-  ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> T e. RR )
10 9 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. RR )
11 10 recnd 
 |-  ( ( 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 oveq2 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( A ` j ) - ( B ` j ) ) = ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) )
24 23 oveq1d 
 |-  ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) ^ 2 ) )
25 subdi 
 |-  ( ( T e. CC /\ ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( T x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( T x. ( A ` j ) ) - ( T x. ( C ` j ) ) ) )
26 25 3coml 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( T x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( T x. ( A ` j ) ) - ( T x. ( C ` j ) ) ) )
27 ax-1cn 
 |-  1 e. CC
28 subcl 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
29 27 28 mpan 
 |-  ( T e. CC -> ( 1 - T ) e. CC )
30 29 adantl 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
31 simpl 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( A ` j ) e. CC )
32 subdir 
 |-  ( ( 1 e. CC /\ ( 1 - T ) e. CC /\ ( A ` j ) e. CC ) -> ( ( 1 - ( 1 - T ) ) x. ( A ` j ) ) = ( ( 1 x. ( A ` j ) ) - ( ( 1 - T ) x. ( A ` j ) ) ) )
33 27 30 31 32 mp3an2i 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( 1 - ( 1 - T ) ) x. ( A ` j ) ) = ( ( 1 x. ( A ` j ) ) - ( ( 1 - T ) x. ( A ` j ) ) ) )
34 nncan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - ( 1 - T ) ) = T )
35 27 34 mpan 
 |-  ( T e. CC -> ( 1 - ( 1 - T ) ) = T )
36 35 oveq1d 
 |-  ( T e. CC -> ( ( 1 - ( 1 - T ) ) x. ( A ` j ) ) = ( T x. ( A ` j ) ) )
37 36 adantl 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( 1 - ( 1 - T ) ) x. ( A ` j ) ) = ( T x. ( A ` j ) ) )
38 mullid 
 |-  ( ( A ` j ) e. CC -> ( 1 x. ( A ` j ) ) = ( A ` j ) )
39 38 oveq1d 
 |-  ( ( A ` j ) e. CC -> ( ( 1 x. ( A ` j ) ) - ( ( 1 - T ) x. ( A ` j ) ) ) = ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) )
40 39 adantr 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( 1 x. ( A ` j ) ) - ( ( 1 - T ) x. ( A ` j ) ) ) = ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) )
41 33 37 40 3eqtr3rd 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) = ( T x. ( A ` j ) ) )
42 41 oveq1d 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) - ( T x. ( C ` j ) ) ) = ( ( T x. ( A ` j ) ) - ( T x. ( C ` j ) ) ) )
43 42 3adant2 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) - ( T x. ( C ` j ) ) ) = ( ( T x. ( A ` j ) ) - ( T x. ( C ` j ) ) ) )
44 simp1 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( A ` j ) e. CC )
45 mulcl 
 |-  ( ( ( 1 - T ) e. CC /\ ( A ` j ) e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC )
46 29 45 sylan 
 |-  ( ( T e. CC /\ ( A ` j ) e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC )
47 46 ancoms 
 |-  ( ( ( A ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC )
48 47 3adant2 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC )
49 mulcl 
 |-  ( ( T e. CC /\ ( C ` j ) e. CC ) -> ( T x. ( C ` j ) ) e. CC )
50 49 ancoms 
 |-  ( ( ( C ` j ) e. CC /\ T e. CC ) -> ( T x. ( C ` j ) ) e. CC )
51 50 3adant1 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( T x. ( C ` j ) ) e. CC )
52 44 48 51 subsub4d 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( A ` j ) - ( ( 1 - T ) x. ( A ` j ) ) ) - ( T x. ( C ` j ) ) ) = ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) )
53 26 43 52 3eqtr2rd 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) = ( T x. ( ( A ` j ) - ( C ` j ) ) ) )
54 53 oveq1d 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) ^ 2 ) = ( ( T x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) )
55 simp3 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> T e. CC )
56 subcl 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
57 56 3adant3 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
58 55 57 sqmuld 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( T x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) = ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
59 54 58 eqtrd 
 |-  ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( A ` j ) - ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) ^ 2 ) = ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
60 24 59 sylan9eqr 
 |-  ( ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) /\ ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) -> ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
61 3 6 12 22 60 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 ) ) -> ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
62 61 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 ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
63 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 )
64 8 resqcld 
 |-  ( T e. ( 0 [,] 1 ) -> ( T ^ 2 ) e. RR )
65 64 recnd 
 |-  ( T e. ( 0 [,] 1 ) -> ( T ^ 2 ) e. CC )
66 65 adantr 
 |-  ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( T ^ 2 ) e. CC )
67 66 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 ^ 2 ) e. CC )
68 2 3adant1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
69 68 3adant2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
70 5 3adant1 
 |-  ( ( N e. NN /\ C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
71 70 3adant2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
72 69 71 subcld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
73 72 sqcld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
74 73 3expa 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
75 74 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 )
76 63 67 75 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 ) ) ) ) ) -> ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( ( T ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
77 62 76 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 ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )