Metamath Proof Explorer

Definition df-perpg

Description: Define the "perpendicular" relation. Definition 8.11 of Schwabhauser p. 59. See isperp . (Contributed by Thierry Arnoux, 8-Sep-2019)

Ref Expression
Assertion df-perpg 
|- perpG = ( 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. ( raG ` g ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cperpg 
 |-  perpG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 va 
 |-  a
4 vb 
 |-  b
5 3 cv 
 |-  a
6 clng 
 |-  LineG
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( LineG ` g )
9 8 crn 
 |-  ran ( LineG ` g )
10 5 9 wcel 
 |-  a e. ran ( LineG ` g )
11 4 cv 
 |-  b
12 11 9 wcel 
 |-  b e. ran ( LineG ` g )
13 10 12 wa 
 |-  ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) )
14 vx 
 |-  x
15 5 11 cin 
 |-  ( a i^i b )
16 vu 
 |-  u
17 vv 
 |-  v
18 16 cv 
 |-  u
19 14 cv 
 |-  x
20 17 cv 
 |-  v
21 18 19 20 cs3 
 |-  <" u x v ">
22 crag 
 |-  raG
23 7 22 cfv 
 |-  ( raG ` g )
24 21 23 wcel 
 |-  <" u x v "> e. ( raG ` g )
25 24 17 11 wral 
 |-  A. v e. b <" u x v "> e. ( raG ` g )
26 25 16 5 wral 
 |-  A. u e. a A. v e. b <" u x v "> e. ( raG ` g )
27 26 14 15 wrex 
 |-  E. x e. ( a i^i b ) A. u e. a A. v e. b <" u x v "> e. ( raG ` g )
28 13 27 wa 
 |-  ( ( 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. ( raG ` g ) )
29 28 3 4 copab 
 |-  { <. 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. ( raG ` g ) ) }
30 1 2 29 cmpt 
 |-  ( 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. ( raG ` g ) ) } )
31 0 30 wceq 
 |-  perpG = ( 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. ( raG ` g ) ) } )