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

Definition df-halfplane 26274
Description: Returns the halplanes delimited by  l. (For my private use only. Don't use.) (Contributed by FL, 16-Sep-2016.)
Assertion
Ref Expression
df-halfplane  |- Halfplane  =  ( g  e. Ibg  |->  ( l  e.  (PLines `  g
)  |->  ( ( (PPoints `  g )  \  l
) /. ( (ss
`  g ) `  l ) ) ) )
Distinct variable group:    g, l

Detailed syntax breakdown of Definition df-halfplane
StepHypRef Expression
1 chalfp 26273 . 2  class Halfplane
2 vg . . 3  set  g
3 cibg 26210 . . 3  class Ibg
4 vl . . . 4  set  l
52cv 1631 . . . . 5  class  g
6 cplines 26161 . . . . 5  class PLines
75, 6cfv 5271 . . . 4  class  (PLines `  g )
8 cpoints 26159 . . . . . . 7  class PPoints
95, 8cfv 5271 . . . . . 6  class  (PPoints `  g
)
104cv 1631 . . . . . 6  class  l
119, 10cdif 3162 . . . . 5  class  ( (PPoints `  g )  \  l
)
12 csas 26265 . . . . . . 7  class ss
135, 12cfv 5271 . . . . . 6  class  (ss `  g )
1410, 13cfv 5271 . . . . 5  class  ( (ss
`  g ) `  l )
1511, 14cqs 6675 . . . 4  class  ( ( (PPoints `  g )  \  l ) /. ( (ss `  g ) `
 l ) )
164, 7, 15cmpt 4093 . . 3  class  ( l  e.  (PLines `  g
)  |->  ( ( (PPoints `  g )  \  l
) /. ( (ss
`  g ) `  l ) ) )
172, 3, 16cmpt 4093 . 2  class  ( g  e. Ibg  |->  ( l  e.  (PLines `  g )  |->  ( ( (PPoints `  g
)  \  l ) /. ( (ss `  g
) `  l )
) ) )
181, 17wceq 1632 1  wff Halfplane  =  ( g  e. Ibg  |->  ( l  e.  (PLines `  g
)  |->  ( ( (PPoints `  g )  \  l
) /. ( (ss
`  g ) `  l ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  aishp  26275
  Copyright terms: Public domain W3C validator