Metamath Proof Explorer

Theorem brbtwn

Description: The binary relation form of the betweenness predicate. The statement A Btwn <. B , C >. should be informally read as " A lies on a line segment between B and C . This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion brbtwn 
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Btwn <. B , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-btwn 
 |-  Btwn = `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) }
2 1 breqi 
 |-  ( A Btwn <. B , C >. <-> A `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <. B , C >. )
3 opex 
 |-  <. B , C >. e. _V
4 brcnvg 
 |-  ( ( A e. ( EE ` N ) /\ <. B , C >. e. _V ) -> ( A `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <. B , C >. <-> <. B , C >. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } A ) )
5 3 4 mpan2 
 |-  ( A e. ( EE ` N ) -> ( A `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <. B , C >. <-> <. B , C >. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } A ) )
6 5 3ad2ant1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <. B , C >. <-> <. B , C >. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } A ) )
7 df-br 
 |-  ( <. B , C >. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } A <-> <. <. B , C >. , A >. e. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } )
8 eleq1 
 |-  ( y = B -> ( y e. ( EE ` n ) <-> B e. ( EE ` n ) ) )
9 8 3anbi1d 
 |-  ( y = B -> ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) <-> ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) ) )
10 fveq1 
 |-  ( y = B -> ( y ` i ) = ( B ` i ) )
11 10 oveq2d 
 |-  ( y = B -> ( ( 1 - t ) x. ( y ` i ) ) = ( ( 1 - t ) x. ( B ` i ) ) )
12 11 oveq1d 
 |-  ( y = B -> ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) )
13 12 eqeq2d 
 |-  ( y = B -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) )
14 13 rexralbidv 
 |-  ( y = B -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) )
15 9 14 anbi12d 
 |-  ( y = B -> ( ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) <-> ( ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) ) )
16 15 rexbidv 
 |-  ( y = B -> ( E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) <-> E. n e. NN ( ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) ) )
17 eleq1 
 |-  ( z = C -> ( z e. ( EE ` n ) <-> C e. ( EE ` n ) ) )
18 17 3anbi2d 
 |-  ( z = C -> ( ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) <-> ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) ) )
19 fveq1 
 |-  ( z = C -> ( z ` i ) = ( C ` i ) )
20 19 oveq2d 
 |-  ( z = C -> ( t x. ( z ` i ) ) = ( t x. ( C ` i ) ) )
21 20 oveq2d 
 |-  ( z = C -> ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) )
22 21 eqeq2d 
 |-  ( z = C -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
23 22 rexralbidv 
 |-  ( z = C -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
24 18 23 anbi12d 
 |-  ( z = C -> ( ( ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) <-> ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
25 24 rexbidv 
 |-  ( z = C -> ( E. n e. NN ( ( B e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( z ` i ) ) ) ) <-> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
26 eleq1 
 |-  ( x = A -> ( x e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
27 26 3anbi3d 
 |-  ( x = A -> ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) <-> ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) ) )
28 fveq1 
 |-  ( x = A -> ( x ` i ) = ( A ` i ) )
29 28 eqeq1d 
 |-  ( x = A -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) <-> ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
30 29 rexralbidv 
 |-  ( x = A -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
31 27 30 anbi12d 
 |-  ( x = A -> ( ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) <-> ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
32 31 rexbidv 
 |-  ( x = A -> ( E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) <-> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
33 16 25 32 eloprabg 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( <. <. B , C >. , A >. e. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <-> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
34 simp1 
 |-  ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) -> B e. ( EE ` n ) )
35 simp1 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> B e. ( EE ` N ) )
36 eedimeq 
 |-  ( ( B e. ( EE ` n ) /\ B e. ( EE ` N ) ) -> n = N )
37 34 35 36 syl2anr 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) ) -> n = N )
38 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
39 38 raleqdv 
 |-  ( n = N -> ( A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) <-> A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
40 39 rexbidv 
 |-  ( n = N -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
41 37 40 syl 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
42 41 biimpd 
 |-  ( ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
43 42 expimpd 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
44 43 rexlimdvw 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
45 eleenn 
 |-  ( B e. ( EE ` N ) -> N e. NN )
46 45 3ad2ant1 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> N e. NN )
47 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
48 47 eleq2d 
 |-  ( n = N -> ( B e. ( EE ` n ) <-> B e. ( EE ` N ) ) )
49 47 eleq2d 
 |-  ( n = N -> ( C e. ( EE ` n ) <-> C e. ( EE ` N ) ) )
50 47 eleq2d 
 |-  ( n = N -> ( A e. ( EE ` n ) <-> A e. ( EE ` N ) ) )
51 48 49 50 3anbi123d 
 |-  ( n = N -> ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) <-> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) )
52 51 40 anbi12d 
 |-  ( n = N -> ( ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) <-> ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
53 52 rspcev 
 |-  ( ( N e. NN /\ ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) -> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
54 53 exp32 
 |-  ( N e. NN -> ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) ) )
55 46 54 mpcom 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) -> E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) ) )
56 44 55 impbid 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( E. n e. NN ( ( B e. ( EE ` n ) /\ C e. ( EE ` n ) /\ A e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
57 33 56 bitrd 
 |-  ( ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( <. <. B , C >. , A >. e. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
58 57 3comr 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( <. <. B , C >. , A >. e. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
59 7 58 syl5bb 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( <. B , C >. { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } A <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
60 6 59 bitrd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A `' { <. <. y , z >. , x >. | E. n e. NN ( ( y e. ( EE ` n ) /\ z e. ( EE ` n ) /\ x e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( x ` i ) = ( ( ( 1 - t ) x. ( y ` i ) ) + ( t x. ( z ` i ) ) ) ) } <. B , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )
61 2 60 syl5bb 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A Btwn <. B , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( C ` i ) ) ) ) )