Metamath Proof Explorer

Definition df-colinear

Description: The colinearity predicate states that the three points in its arguments sit on one line. Definition 4.10 of Schwabhauser p. 36. (Contributed by Scott Fenton, 25-Oct-2013)

Ref Expression
Assertion df-colinear 
|- Colinear = `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccolin 
 |-  Colinear
1 vb 
 |-  b
2 vc 
 |-  c
3 va 
 |-  a
4 vn 
 |-  n
5 cn 
 |-  NN
6 3 cv 
 |-  a
7 cee 
 |-  EE
8 4 cv 
 |-  n
9 8 7 cfv 
 |-  ( EE ` n )
10 6 9 wcel 
 |-  a e. ( EE ` n )
11 1 cv 
 |-  b
12 11 9 wcel 
 |-  b e. ( EE ` n )
13 2 cv 
 |-  c
14 13 9 wcel 
 |-  c e. ( EE ` n )
15 10 12 14 w3a 
 |-  ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) )
16 cbtwn 
 |-  Btwn
17 11 13 cop 
 |-  <. b , c >.
18 6 17 16 wbr 
 |-  a Btwn <. b , c >.
19 13 6 cop 
 |-  <. c , a >.
20 11 19 16 wbr 
 |-  b Btwn <. c , a >.
21 6 11 cop 
 |-  <. a , b >.
22 13 21 16 wbr 
 |-  c Btwn <. a , b >.
23 18 20 22 w3o 
 |-  ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. )
24 15 23 wa 
 |-  ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) )
25 24 4 5 wrex 
 |-  E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) )
26 25 1 2 3 coprab 
 |-  { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) }
27 26 ccnv 
 |-  `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) }
28 0 27 wceq 
 |-  Colinear = `' { <. <. b , c >. , a >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ c e. ( EE ` n ) ) /\ ( a Btwn <. b , c >. \/ b Btwn <. c , a >. \/ c Btwn <. a , b >. ) ) }