Metamath Proof Explorer

Definition df-btwn

Description: Define the Euclidean betweenness predicate. For details, see brbtwn . (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion df-btwn 
|- Btwn = `' { <. <. x , z >. , y >. | E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbtwn 
 |-  Btwn
1 vx 
 |-  x
2 vz 
 |-  z
3 vy 
 |-  y
4 vn 
 |-  n
5 cn 
 |-  NN
6 1 cv 
 |-  x
7 cee 
 |-  EE
8 4 cv 
 |-  n
9 8 7 cfv 
 |-  ( EE ` n )
10 6 9 wcel 
 |-  x e. ( EE ` n )
11 2 cv 
 |-  z
12 11 9 wcel 
 |-  z e. ( EE ` n )
13 3 cv 
 |-  y
14 13 9 wcel 
 |-  y e. ( EE ` n )
15 10 12 14 w3a 
 |-  ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) )
16 vt 
 |-  t
17 cc0 
 |-  0
18 cicc 
 |-  [,]
19 c1 
 |-  1
20 17 19 18 co 
 |-  ( 0 [,] 1 )
21 vi 
 |-  i
22 cfz 
 |-  ...
23 19 8 22 co 
 |-  ( 1 ... n )
24 21 cv 
 |-  i
25 24 13 cfv 
 |-  ( y ` i )
26 cmin 
 |-  -
27 16 cv 
 |-  t
28 19 27 26 co 
 |-  ( 1 - t )
29 cmul 
 |-  x.
30 24 6 cfv 
 |-  ( x ` i )
31 28 30 29 co 
 |-  ( ( 1 - t ) x. ( x ` i ) )
32 caddc 
 |-  +
33 24 11 cfv 
 |-  ( z ` i )
34 27 33 29 co 
 |-  ( t x. ( z ` i ) )
35 31 34 32 co 
 |-  ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
36 25 35 wceq 
 |-  ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
37 36 21 23 wral 
 |-  A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
38 37 16 20 wrex 
 |-  E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
39 15 38 wa 
 |-  ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) )
40 39 4 5 wrex 
 |-  E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) )
41 40 1 2 3 coprab 
 |-  { <. <. x , z >. , y >. | E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) ) }
42 41 ccnv 
 |-  `' { <. <. x , z >. , y >. | E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) ) }
43 0 42 wceq 
 |-  Btwn = `' { <. <. x , z >. , y >. | E. n e. NN ( ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) ) /\ E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) ) ) }