Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sside Unicode version

Definition df-sside 25329
Description: Two points not on  l are on the same side of  l if the segment xy doesn't intersect  l. Definition 10 of [AitkenIBG] p. 4 (For my private use only. Don't use.) (Contributed by FL, 26-May-2016.)
Assertion
Ref Expression
df-sside  |- ss  =  ( g  e. Ibg  |->  ( l  e.  (PLines `  g
)  |->  { <. x ,  y >.  |  ( x  e.  ( (PPoints `  g )  \  l
)  /\  y  e.  ( (PPoints `  g )  \  l )  /\  ( ( x ( seg `  g ) y )  i^i  l
)  =  (/) ) } ) )
Distinct variable group:    g, l, x, y

Detailed syntax breakdown of Definition df-sside
StepHypRef Expression
1 csas 25328 . 2  class ss
2 vg . . 3  set  g
3 cibg 25273 . . 3  class Ibg
4 vl . . . 4  set  l
52cv 1618 . . . . 5  class  g
6 cplines 25224 . . . . 5  class PLines
75, 6cfv 4592 . . . 4  class  (PLines `  g )
8 vx . . . . . . . 8  set  x
98cv 1618 . . . . . . 7  class  x
10 cpoints 25222 . . . . . . . . 9  class PPoints
115, 10cfv 4592 . . . . . . . 8  class  (PPoints `  g
)
124cv 1618 . . . . . . . 8  class  l
1311, 12cdif 3075 . . . . . . 7  class  ( (PPoints `  g )  \  l
)
149, 13wcel 1621 . . . . . 6  wff  x  e.  ( (PPoints `  g
)  \  l )
15 vy . . . . . . . 8  set  y
1615cv 1618 . . . . . . 7  class  y
1716, 13wcel 1621 . . . . . 6  wff  y  e.  ( (PPoints `  g
)  \  l )
18 cseg 25296 . . . . . . . . . 10  class  seg
195, 18cfv 4592 . . . . . . . . 9  class  ( seg `  g )
209, 16, 19co 5710 . . . . . . . 8  class  ( x ( seg `  g
) y )
2120, 12cin 3077 . . . . . . 7  class  ( ( x ( seg `  g
) y )  i^i  l )
22 c0 3362 . . . . . . 7  class  (/)
2321, 22wceq 1619 . . . . . 6  wff  ( ( x ( seg `  g
) y )  i^i  l )  =  (/)
2414, 17, 23w3a 939 . . . . 5  wff  ( x  e.  ( (PPoints `  g
)  \  l )  /\  y  e.  (
(PPoints `  g )  \ 
l )  /\  (
( x ( seg `  g ) y )  i^i  l )  =  (/) )
2524, 8, 15copab 3973 . . . 4  class  { <. x ,  y >.  |  ( x  e.  ( (PPoints `  g )  \  l
)  /\  y  e.  ( (PPoints `  g )  \  l )  /\  ( ( x ( seg `  g ) y )  i^i  l
)  =  (/) ) }
264, 7, 25cmpt 3974 . . 3  class  ( l  e.  (PLines `  g
)  |->  { <. x ,  y >.  |  ( x  e.  ( (PPoints `  g )  \  l
)  /\  y  e.  ( (PPoints `  g )  \  l )  /\  ( ( x ( seg `  g ) y )  i^i  l
)  =  (/) ) } )
272, 3, 26cmpt 3974 . 2  class  ( g  e. Ibg  |->  ( l  e.  (PLines `  g )  |->  { <. x ,  y
>.  |  ( x  e.  ( (PPoints `  g
)  \  l )  /\  y  e.  (
(PPoints `  g )  \ 
l )  /\  (
( x ( seg `  g ) y )  i^i  l )  =  (/) ) } ) )
281, 27wceq 1619 1  wff ss  =  ( g  e. Ibg  |->  ( l  e.  (PLines `  g
)  |->  { <. x ,  y >.  |  ( x  e.  ( (PPoints `  g )  \  l
)  /\  y  e.  ( (PPoints `  g )  \  l )  /\  ( ( x ( seg `  g ) y )  i^i  l
)  =  (/) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  isside0  25330
  Copyright terms: Public domain W3C validator