Metamath Proof Explorer

Theorem axsegcon

Description: Any segment A B can be extended to a point x such that B x is congruent to C D . Axiom A4 of Schwabhauser p. 11. (Contributed by Scott Fenton, 4-Jun-2013)

Ref Expression
Assertion axsegcon 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 1 ex 
 |-  ( 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 ) ) ) )
3 simprll 
 |-  ( ( A =/= B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> A e. ( EE ` N ) )
4 simprlr 
 |-  ( ( A =/= B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> B e. ( EE ` N ) )
5 simpl 
 |-  ( ( A =/= B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> A =/= B )
6 simprr 
 |-  ( ( A =/= B /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
7 eqid 
 |-  sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
8 eqid 
 |-  sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
9 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) )
10 7 8 9 axsegconlem8 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) e. ( EE ` N ) )
11 7 8 axsegconlem7 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) e. ( 0 [,] 1 ) )
12 7 8 9 axsegconlem10 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) )
13 7 8 9 axsegconlem9 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
14 fveq1 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) )
15 14 oveq2d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( t x. ( x ` i ) ) = ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) )
16 15 oveq2d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) )
17 16 eqeq2d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) ) )
18 17 ralbidv 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( 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. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) ) )
19 14 oveq2d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( ( B ` i ) - ( x ` i ) ) = ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) )
20 19 oveq1d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) )
21 20 sumeq2sdv 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) )
22 21 eqeq1d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( 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 ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
23 18 22 anbi12d 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) -> ( ( 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. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
24 oveq2 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( 1 - t ) = ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) )
25 24 oveq1d 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( ( 1 - t ) x. ( A ` i ) ) = ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) )
26 oveq1 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) = ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) )
27 25 26 oveq12d 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) )
28 27 eqeq2d 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) ) )
29 28 ralbidv 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) ) )
30 29 anbi1d 
 |-  ( t = ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) <-> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) )
31 23 30 rspc2ev 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) e. ( EE ` N ) /\ ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) e. ( 0 [,] 1 ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) ) x. ( A ` i ) ) + ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) / ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` i ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) + ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) ) x. ( B ` k ) ) - ( ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) ) x. ( A ` k ) ) ) / ( sqrt ` sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) ) ) ) ` 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. ( 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 ) ) )
32 10 11 12 13 31 syl112anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( 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 ) ) )
33 3 4 5 6 32 syl31anc 
 |-  ( ( 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 ) ) )
34 33 ex 
 |-  ( 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 ) ) ) )
35 2 34 pm2.61ine 
 |-  ( ( ( 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 ) ) )
36 simpllr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
37 simplll 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
38 simpr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
39 brbtwn 
 |-  ( ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( B Btwn <. A , x >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( B Btwn <. A , x >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( x ` i ) ) ) ) )
41 simplrl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> C e. ( EE ` N ) )
42 simplrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> D e. ( EE ` N ) )
43 brcgr 
 |-  ( ( ( B e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. B , x >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
44 36 38 41 42 43 syl22anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( <. B , x >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( x ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
45 40 44 anbi12d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) <-> ( 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 ) ) ) )
46 r19.41v 
 |-  ( 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. 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 ) ) )
47 45 46 bitr4di 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) <-> 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 ) ) ) )
48 47 rexbidva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) <-> 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 ) ) ) )
49 35 48 mpbird 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) )
50 49 3adant1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. B , x >. Cgr <. C , D >. ) )