Definition df-btwn 24018

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

Assertion

Ref	Expression
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 ) ) ) ) }

Distinct variable group:   x, n, y, z, t, i

Detailed syntax breakdown of Definition df-btwn

Step	Hyp	Ref	Expression
1		cbtwn 24015	. 2 class Btwn
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1378	. . . . . . . 8 class x
4		vn	. . . . . . . . . 10 setvar n
5	4	cv 1378	. . . . . . . . 9 class n
6		cee 24014	. . . . . . . . 9 class EE
7	5, 6	cfv 5594	. . . . . . . 8 class ( EE ` n )
8	3, 7	wcel 1767	. . . . . . 7 wff x e. ( EE ` n )
9		vz	. . . . . . . . 9 setvar z
10	9	cv 1378	. . . . . . . 8 class z
11	10, 7	wcel 1767	. . . . . . 7 wff z e. ( EE ` n )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1378	. . . . . . . 8 class y
14	13, 7	wcel 1767	. . . . . . 7 wff y e. ( EE ` n )
15	8, 11, 14	w3a 973	. . . . . 6 wff ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) )
16		vi	. . . . . . . . . . 11 setvar i
17	16	cv 1378	. . . . . . . . . 10 class i
18	17, 13	cfv 5594	. . . . . . . . 9 class ( y ` i )
19		c1 9505	. . . . . . . . . . . 12 class 1
20		vt	. . . . . . . . . . . . 13 setvar t
21	20	cv 1378	. . . . . . . . . . . 12 class t
22		cmin 9817	. . . . . . . . . . . 12 class -
23	19, 21, 22	co 6295	. . . . . . . . . . 11 class ( 1 - t )
24	17, 3	cfv 5594	. . . . . . . . . . 11 class ( x ` i )
25		cmul 9509	. . . . . . . . . . 11 class x.
26	23, 24, 25	co 6295	. . . . . . . . . 10 class ( ( 1 - t ) x. ( x ` i ) )
27	17, 10	cfv 5594	. . . . . . . . . . 11 class ( z ` i )
28	21, 27, 25	co 6295	. . . . . . . . . 10 class ( t x. ( z ` i ) )
29		caddc 9507	. . . . . . . . . 10 class +
30	26, 28, 29	co 6295	. . . . . . . . 9 class ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
31	18, 30	wceq 1379	. . . . . . . 8 wff ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
32		cfz 11684	. . . . . . . . 9 class ...
33	19, 5, 32	co 6295	. . . . . . . 8 class ( 1 ... n )
34	31, 16, 33	wral 2817	. . . . . . 7 wff A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
35		cc0 9504	. . . . . . . 8 class 0
36		cicc 11544	. . . . . . . 8 class [,]
37	35, 19, 36	co 6295	. . . . . . 7 class ( 0 [,] 1 )
38	34, 20, 37	wrex 2818	. . . . . 6 wff 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 369	. . . . 5 wff ( ( 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		cn 10548	. . . . 5 class NN
41	39, 4, 40	wrex 2818	. . . 4 wff 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, 2, 9, 12	coprab 6296	. . 3 class { <. <. 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	42	ccnv 5004	. 2 class `' { <. <. 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 ) ) ) ) }
44	1, 43	wceq 1379	1 wff 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 ) ) ) ) }

This definition is referenced by:  brbtwn  24025