Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-colinear Unicode version

Definition df-colinear 24072
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.)
Assertion
Ref Expression
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
>. ) ) }
Distinct variable group:    a, b, c, n

Detailed syntax breakdown of Definition df-colinear
StepHypRef Expression
1 ccolin 24068 . 2  class  Colinear
2 va . . . . . . . . 9  set  a
32cv 1623 . . . . . . . 8  class  a
4 vn . . . . . . . . . 10  set  n
54cv 1623 . . . . . . . . 9  class  n
6 cee 23924 . . . . . . . . 9  class  EE
75, 6cfv 5222 . . . . . . . 8  class  ( EE
`  n )
83, 7wcel 1685 . . . . . . 7  wff  a  e.  ( EE `  n
)
9 vb . . . . . . . . 9  set  b
109cv 1623 . . . . . . . 8  class  b
1110, 7wcel 1685 . . . . . . 7  wff  b  e.  ( EE `  n
)
12 vc . . . . . . . . 9  set  c
1312cv 1623 . . . . . . . 8  class  c
1413, 7wcel 1685 . . . . . . 7  wff  c  e.  ( EE `  n
)
158, 11, 14w3a 936 . . . . . 6  wff  ( a  e.  ( EE `  n )  /\  b  e.  ( EE `  n
)  /\  c  e.  ( EE `  n ) )
1610, 13cop 3645 . . . . . . . 8  class  <. b ,  c >.
17 cbtwn 23925 . . . . . . . 8  class  Btwn
183, 16, 17wbr 4025 . . . . . . 7  wff  a  Btwn  <.
b ,  c >.
1913, 3cop 3645 . . . . . . . 8  class  <. c ,  a >.
2010, 19, 17wbr 4025 . . . . . . 7  wff  b  Btwn  <.
c ,  a >.
213, 10cop 3645 . . . . . . . 8  class  <. a ,  b >.
2213, 21, 17wbr 4025 . . . . . . 7  wff  c  Btwn  <.
a ,  b >.
2318, 20, 22w3o 935 . . . . . 6  wff  ( a 
Btwn  <. b ,  c
>.  \/  b  Btwn  <. c ,  a >.  \/  c  Btwn  <. a ,  b
>. )
2415, 23wa 360 . . . . 5  wff  ( ( 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 cn 9742 . . . . 5  class  NN
2624, 4, 25wrex 2546 . . . 4  wff  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
>. ) )
2726, 9, 12, 2coprab 5821 . . 3  class  { <. <.
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
>. ) ) }
2827ccnv 4688 . 2  class  `' { <. <. 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
>. ) ) }
291, 28wceq 1624 1  wff  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
>. ) ) }
Colors of variables: wff set class
This definition is referenced by:  colinrel  24088  brcolinear2  24089  colinearex  24091  colineardim1  24092
  Copyright terms: Public domain W3C validator