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

Definition df-perpg 24820
Description: Define the "perpendicular" relation. Definition 8.11 of [Schwabhauser] p. 59. See isperp 24836. (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 24819 . 2  class ⟂G
2 vg . . 3  setvar  g
3 cvv 3031 . . 3  class  _V
4 va . . . . . . . 8  setvar  a
54cv 1451 . . . . . . 7  class  a
62cv 1451 . . . . . . . . 9  class  g
7 clng 24564 . . . . . . . . 9  class LineG
86, 7cfv 5589 . . . . . . . 8  class  (LineG `  g )
98crn 4840 . . . . . . 7  class  ran  (LineG `  g )
105, 9wcel 1904 . . . . . 6  wff  a  e. 
ran  (LineG `  g )
11 vb . . . . . . . 8  setvar  b
1211cv 1451 . . . . . . 7  class  b
1312, 9wcel 1904 . . . . . 6  wff  b  e. 
ran  (LineG `  g )
1410, 13wa 376 . . . . 5  wff  ( a  e.  ran  (LineG `  g )  /\  b  e.  ran  (LineG `  g
) )
15 vu . . . . . . . . . . 11  setvar  u
1615cv 1451 . . . . . . . . . 10  class  u
17 vx . . . . . . . . . . 11  setvar  x
1817cv 1451 . . . . . . . . . 10  class  x
19 vv . . . . . . . . . . 11  setvar  v
2019cv 1451 . . . . . . . . . 10  class  v
2116, 18, 20cs3 12997 . . . . . . . . 9  class  <" u x v ">
22 crag 24817 . . . . . . . . . 10  class ∟G
236, 22cfv 5589 . . . . . . . . 9  class  (∟G `  g
)
2421, 23wcel 1904 . . . . . . . 8  wff  <" u x v ">  e.  (∟G `  g )
2524, 19, 12wral 2756 . . . . . . 7  wff  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
2625, 15, 5wral 2756 . . . . . 6  wff  A. u  e.  a  A. v  e.  b  <" u x v ">  e.  (∟G `  g )
275, 12cin 3389 . . . . . 6  class  ( a  i^i  b )
2826, 17, 27wrex 2757 . . . . 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 376 . . . 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 4453 . . 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 4454 . 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 1452 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  24834  perpln2  24835  isperp  24836
  Copyright terms: Public domain W3C validator