MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-perpg Structured version   Unicode version

Definition df-perpg 24218
Description: Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 8-Sep-2019.)
Assertion
Ref Expression
df-perpg  |- ⟂G  =  ( g  e.  _V  |->  {
<. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
) } )
Distinct variable group:    a, b, u, v, x, g

Detailed syntax breakdown of Definition df-perpg
StepHypRef Expression
1 cperpg 24217 . 2  class ⟂G
2 vg . . 3  setvar  g
3 cvv 3051 . . 3  class  _V
4 va . . . . . . . 8  setvar  a
54cv 1398 . . . . . . 7  class  a
62cv 1398 . . . . . . . . 9  class  g
7 clng 23973 . . . . . . . . 9  class LineG
86, 7cfv 5513 . . . . . . . 8  class  (LineG `  g )
98crn 4931 . . . . . . 7  class  ran  (LineG `  g )
105, 9wcel 1836 . . . . . 6  wff  a  e. 
ran  (LineG `  g )
11 vb . . . . . . . 8  setvar  b
1211cv 1398 . . . . . . 7  class  b
1312, 9wcel 1836 . . . . . 6  wff  b  e. 
ran  (LineG `  g )
1410, 13wa 367 . . . . 5  wff  ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )
15 vu . . . . . . . . . . 11  setvar  u
1615cv 1398 . . . . . . . . . 10  class  u
17 vx . . . . . . . . . . 11  setvar  x
1817cv 1398 . . . . . . . . . 10  class  x
19 vv . . . . . . . . . . 11  setvar  v
2019cv 1398 . . . . . . . . . 10  class  v
2116, 18, 20cs3 12741 . . . . . . . . 9  class  <" u x v ">
22 crag 24215 . . . . . . . . . 10  class ∟G
236, 22cfv 5513 . . . . . . . . 9  class  (∟G `  g
)
2421, 23wcel 1836 . . . . . . . 8  wff  <" u x v ">  e.  (∟G `  g )
2524, 19, 12wral 2746 . . . . . . 7  wff  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
2625, 15, 5wral 2746 . . . . . 6  wff  A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
275, 12cin 3405 . . . . . 6  class  ( a  i^i  b )
2826, 17, 27wrex 2747 . . . . 5  wff  E. x  e.  ( a  i^i  b
) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
2914, 28wa 367 . . . 4  wff  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
)
3029, 4, 11copab 4441 . . 3  class  { <. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g
) ) }
312, 3, 30cmpt 4442 . 2  class  ( g  e.  _V  |->  { <. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g ) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g
) ) } )
321, 31wceq 1399 1  wff ⟂G  =  ( g  e.  _V  |->  {
<. a ,  b >.  |  ( ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )  /\  E. x  e.  ( a  i^i  b ) A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
) } )
Colors of variables: wff setvar class
This definition is referenced by:  perpln1  24232  perpln2  24233  isperp  24234
  Copyright terms: Public domain W3C validator