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

Definition df-line2 30953
Description: Define the Line function. This function generates the line passing through the distinct points  a and  b. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.)
Assertion
Ref Expression
df-line2  |- Line  =  { <. <. a ,  b
>. ,  l >.  |  E. n  e.  NN  ( ( a  e.  ( EE `  n
)  /\  b  e.  ( EE `  n )  /\  a  =/=  b
)  /\  l  =  [ <. a ,  b
>. ] `'  Colinear  ) }
Distinct variable group:    a, b, l, n

Detailed syntax breakdown of Definition df-line2
StepHypRef Expression
1 cline2 30950 . 2  class Line
2 va . . . . . . . 8  setvar  a
32cv 1454 . . . . . . 7  class  a
4 vn . . . . . . . . 9  setvar  n
54cv 1454 . . . . . . . 8  class  n
6 cee 24967 . . . . . . . 8  class  EE
75, 6cfv 5601 . . . . . . 7  class  ( EE
`  n )
83, 7wcel 1898 . . . . . 6  wff  a  e.  ( EE `  n
)
9 vb . . . . . . . 8  setvar  b
109cv 1454 . . . . . . 7  class  b
1110, 7wcel 1898 . . . . . 6  wff  b  e.  ( EE `  n
)
123, 10wne 2633 . . . . . 6  wff  a  =/=  b
138, 11, 12w3a 991 . . . . 5  wff  ( a  e.  ( EE `  n )  /\  b  e.  ( EE `  n
)  /\  a  =/=  b )
14 vl . . . . . . 7  setvar  l
1514cv 1454 . . . . . 6  class  l
163, 10cop 3986 . . . . . . 7  class  <. a ,  b >.
17 ccolin 30853 . . . . . . . 8  class  Colinear
1817ccnv 4852 . . . . . . 7  class  `'  Colinear
1916, 18cec 7387 . . . . . 6  class  [ <. a ,  b >. ] `'  Colinear
2015, 19wceq 1455 . . . . 5  wff  l  =  [ <. a ,  b
>. ] `'  Colinear
2113, 20wa 375 . . . 4  wff  ( ( a  e.  ( EE
`  n )  /\  b  e.  ( EE `  n )  /\  a  =/=  b )  /\  l  =  [ <. a ,  b
>. ] `'  Colinear  )
22 cn 10637 . . . 4  class  NN
2321, 4, 22wrex 2750 . . 3  wff  E. n  e.  NN  ( ( a  e.  ( EE `  n )  /\  b  e.  ( EE `  n
)  /\  a  =/=  b )  /\  l  =  [ <. a ,  b
>. ] `'  Colinear  )
2423, 2, 9, 14coprab 6316 . 2  class  { <. <.
a ,  b >. ,  l >.  |  E. n  e.  NN  (
( a  e.  ( EE `  n )  /\  b  e.  ( EE `  n )  /\  a  =/=  b
)  /\  l  =  [ <. a ,  b
>. ] `'  Colinear  ) }
251, 24wceq 1455 1  wff Line  =  { <. <. a ,  b
>. ,  l >.  |  E. n  e.  NN  ( ( a  e.  ( EE `  n
)  /\  b  e.  ( EE `  n )  /\  a  =/=  b
)  /\  l  =  [ <. a ,  b
>. ] `'  Colinear  ) }
Colors of variables: wff setvar class
This definition is referenced by:  funline  30958  linedegen  30959  fvline  30960  ellines  30968
  Copyright terms: Public domain W3C validator