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 LineG LineG ∟G
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-perpg
StepHypRef Expression
1 cperpg 24819 . 2 ⟂G
2 vg . . 3
3 cvv 3031 . . 3
4 va . . . . . . . 8
54cv 1451 . . . . . . 7
62cv 1451 . . . . . . . . 9
7 clng 24564 . . . . . . . . 9 LineG
86, 7cfv 5589 . . . . . . . 8 LineG
98crn 4840 . . . . . . 7 LineG
105, 9wcel 1904 . . . . . 6 LineG
11 vb . . . . . . . 8
1211cv 1451 . . . . . . 7
1312, 9wcel 1904 . . . . . 6 LineG
1410, 13wa 376 . . . . 5 LineG LineG
15 vu . . . . . . . . . . 11
1615cv 1451 . . . . . . . . . 10
17 vx . . . . . . . . . . 11
1817cv 1451 . . . . . . . . . 10
19 vv . . . . . . . . . . 11
2019cv 1451 . . . . . . . . . 10
2116, 18, 20cs3 12997 . . . . . . . . 9
22 crag 24817 . . . . . . . . . 10 ∟G
236, 22cfv 5589 . . . . . . . . 9 ∟G
2421, 23wcel 1904 . . . . . . . 8 ∟G
2524, 19, 12wral 2756 . . . . . . 7 ∟G
2625, 15, 5wral 2756 . . . . . 6 ∟G
275, 12cin 3389 . . . . . 6
2826, 17, 27wrex 2757 . . . . 5 ∟G
2914, 28wa 376 . . . 4 LineG LineG ∟G
3029, 4, 11copab 4453 . . 3 LineG LineG ∟G
312, 3, 30cmpt 4454 . 2 LineG LineG ∟G
321, 31wceq 1452 1 ⟂G LineG LineG ∟G
 Colors of variables: wff setvar class This definition is referenced by:  perpln1  24834  perpln2  24835  isperp  24836
 Copyright terms: Public domain W3C validator