Definition df-btwn 23138

Description: Define the Euclidean betweenness predicate. For details, see brbtwn 23145. (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 23135	. 2 class Btwn
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1368	. . . . . . . 8 class x
4		vn	. . . . . . . . . 10 setvar n
5	4	cv 1368	. . . . . . . . 9 class n
6		cee 23134	. . . . . . . . 9 class EE
7	5, 6	cfv 5418	. . . . . . . 8 class ( EE ` n )
8	3, 7	wcel 1756	. . . . . . 7 wff x e. ( EE ` n )
9		vz	. . . . . . . . 9 setvar z
10	9	cv 1368	. . . . . . . 8 class z
11	10, 7	wcel 1756	. . . . . . 7 wff z e. ( EE ` n )
12		vy	. . . . . . . . 9 setvar y
13	12	cv 1368	. . . . . . . 8 class y
14	13, 7	wcel 1756	. . . . . . 7 wff y e. ( EE ` n )
15	8, 11, 14	w3a 965	. . . . . 6 wff ( x e. ( EE ` n ) /\ z e. ( EE ` n ) /\ y e. ( EE ` n ) )
16		vi	. . . . . . . . . . 11 setvar i
17	16	cv 1368	. . . . . . . . . 10 class i
18	17, 13	cfv 5418	. . . . . . . . 9 class ( y ` i )
19		c1 9283	. . . . . . . . . . . 12 class 1
20		vt	. . . . . . . . . . . . 13 setvar t
21	20	cv 1368	. . . . . . . . . . . 12 class t
22		cmin 9595	. . . . . . . . . . . 12 class -
23	19, 21, 22	co 6091	. . . . . . . . . . 11 class ( 1 - t )
24	17, 3	cfv 5418	. . . . . . . . . . 11 class ( x ` i )
25		cmul 9287	. . . . . . . . . . 11 class x.
26	23, 24, 25	co 6091	. . . . . . . . . 10 class ( ( 1 - t ) x. ( x ` i ) )
27	17, 10	cfv 5418	. . . . . . . . . . 11 class ( z ` i )
28	21, 27, 25	co 6091	. . . . . . . . . 10 class ( t x. ( z ` i ) )
29		caddc 9285	. . . . . . . . . 10 class +
30	26, 28, 29	co 6091	. . . . . . . . 9 class ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
31	18, 30	wceq 1369	. . . . . . . 8 wff ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
32		cfz 11437	. . . . . . . . 9 class ...
33	19, 5, 32	co 6091	. . . . . . . 8 class ( 1 ... n )
34	31, 16, 33	wral 2715	. . . . . . 7 wff A. i e. ( 1 ... n ) ( y ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( z ` i ) ) )
35		cc0 9282	. . . . . . . 8 class 0
36		cicc 11303	. . . . . . . 8 class [,]
37	35, 19, 36	co 6091	. . . . . . 7 class ( 0 [,] 1 )
38	34, 20, 37	wrex 2716	. . . . . 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 10322	. . . . 5 class NN
41	39, 4, 40	wrex 2716	. . . 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 6092	. . 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 4839	. 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 1369	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  23145