Metamath Proof Explorer

Theorem axsegconlem1

Description: Lemma for axsegcon . Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 fveere 
 |-  ( ( B e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
2 1 3ad2antl1 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
3 fveere 
 |-  ( ( C e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. RR )
4 3 3ad2antl2 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. RR )
5 fveere 
 |-  ( ( D e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( D ` k ) e. RR )
6 5 3ad2antl3 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( D ` k ) e. RR )
7 4 6 resubcld 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( ( C ` k ) - ( D ` k ) ) e. RR )
8 2 7 resubcld 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ k e. ( 1 ... N ) ) -> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) e. RR )
9 8 ralrimiva 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> A. k e. ( 1 ... N ) ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) e. RR )
10 eleenn 
 |-  ( B e. ( EE ` N ) -> N e. NN )
11 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) e. RR ) )
12 10 11 syl 
 |-  ( B e. ( EE ` N ) -> ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) e. RR ) )
13 12 3ad2ant1 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) e. RR ) )
14 9 13 mpbird 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) )
15 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
16 15 3ad2antl1 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
17 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
18 17 3ad2antl2 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
19 fveecn 
 |-  ( ( D e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( D ` i ) e. CC )
20 19 3ad2antl3 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( D ` i ) e. CC )
21 1m0e1 
 |-  ( 1 - 0 ) = 1
22 21 oveq1i 
 |-  ( ( 1 - 0 ) x. ( B ` i ) ) = ( 1 x. ( B ` i ) )
23 mullid 
 |-  ( ( B ` i ) e. CC -> ( 1 x. ( B ` i ) ) = ( B ` i ) )
24 23 3ad2ant1 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( 1 x. ( B ` i ) ) = ( B ` i ) )
25 22 24 eqtrid 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( ( 1 - 0 ) x. ( B ` i ) ) = ( B ` i ) )
26 subcl 
 |-  ( ( ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( ( C ` i ) - ( D ` i ) ) e. CC )
27 subcl 
 |-  ( ( ( B ` i ) e. CC /\ ( ( C ` i ) - ( D ` i ) ) e. CC ) -> ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) e. CC )
28 26 27 sylan2 
 |-  ( ( ( B ` i ) e. CC /\ ( ( C ` i ) e. CC /\ ( D ` i ) e. CC ) ) -> ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) e. CC )
29 28 3impb 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) e. CC )
30 29 mul02d 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) = 0 )
31 25 30 oveq12d 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) = ( ( B ` i ) + 0 ) )
32 addrid 
 |-  ( ( B ` i ) e. CC -> ( ( B ` i ) + 0 ) = ( B ` i ) )
33 32 3ad2ant1 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( ( B ` i ) + 0 ) = ( B ` i ) )
34 31 33 eqtr2d 
 |-  ( ( ( B ` i ) e. CC /\ ( C ` i ) e. CC /\ ( D ` i ) e. CC ) -> ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) )
35 16 18 20 34 syl3anc 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) )
36 35 ralrimiva 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) )
37 18 20 subcld 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( C ` i ) - ( D ` i ) ) e. CC )
38 16 37 nncand 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) = ( ( C ` i ) - ( D ` i ) ) )
39 38 oveq1d 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
40 39 sumeq2dv 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
41 0elunit 
 |-  0 e. ( 0 [,] 1 )
42 fveq1 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) ` i ) )
43 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
44 fveq2 
 |-  ( k = i -> ( C ` k ) = ( C ` i ) )
45 fveq2 
 |-  ( k = i -> ( D ` k ) = ( D ` i ) )
46 44 45 oveq12d 
 |-  ( k = i -> ( ( C ` k ) - ( D ` k ) ) = ( ( C ` i ) - ( D ` i ) ) )
47 43 46 oveq12d 
 |-  ( k = i -> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) = ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) )
48 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) )
49 ovex 
 |-  ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) e. _V
50 47 48 49 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) ` i ) = ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) )
51 42 50 sylan9eq 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) )
52 51 oveq2d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( t x. ( x ` i ) ) = ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) )
53 52 oveq2d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) )
54 53 eqeq2d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) ) )
55 54 ralbidva 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) ) )
56 51 oveq2d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) - ( x ` i ) ) = ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) )
57 56 oveq1d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) )
58 57 sumeq2dv 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) )
59 58 eqeq1d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
60 55 59 anbi12d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) <-> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
61 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
62 61 oveq1d 
 |-  ( t = 0 -> ( ( 1 - t ) x. ( B ` i ) ) = ( ( 1 - 0 ) x. ( B ` i ) ) )
63 oveq1 
 |-  ( t = 0 -> ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) = ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) )
64 62 63 oveq12d 
 |-  ( t = 0 -> ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) )
65 64 eqeq2d 
 |-  ( t = 0 -> ( ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) <-> ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) ) )
66 65 ralbidv 
 |-  ( t = 0 -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) ) )
67 66 anbi1d 
 |-  ( t = 0 -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) <-> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
68 60 67 rspc2ev 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) /\ 0 e. ( 0 [,] 1 ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
69 41 68 mp3an2 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( B ` k ) - ( ( C ` k ) - ( D ` k ) ) ) ) e. ( EE ` N ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - 0 ) x. ( B ` i ) ) + ( 0 x. ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( B ` i ) - ( ( C ` i ) - ( D ` i ) ) ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
70 14 36 40 69 syl12anc 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
71 70 3expb 
 |-  ( ( B e. ( EE ` N ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
72 71 adantll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
73 fveq1 
 |-  ( A = B -> ( A ` i ) = ( B ` i ) )
74 73 oveq2d 
 |-  ( A = B -> ( ( 1 - t ) x. ( A ` i ) ) = ( ( 1 - t ) x. ( B ` i ) ) )
75 74 oveq1d 
 |-  ( A = B -> ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) )
76 75 eqeq2d 
 |-  ( A = B -> ( ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) ) )
77 76 ralbidv 
 |-  ( A = B -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) ) )
78 77 anbi1d 
 |-  ( A = B -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) <-> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
79 78 2rexbidv 
 |-  ( A = B -> ( E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) <-> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
80 72 79 imbitrrid 
 |-  ( A = B -> ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
81 80 imp 
 |-  ( ( A = B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> E. x e. ( EE ` N ) E. t e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )