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

Definition df-rag 24818
 Description: Define the class of right angles. Definition 8.1 of [Schwabhauser] p. 57. See israg 24821. (Contributed by Thierry Arnoux, 25-Aug-2019.)
Assertion
Ref Expression
df-rag ∟G Word pInvG
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rag
StepHypRef Expression
1 crag 24817 . 2 ∟G
2 vg . . 3
3 cvv 3031 . . 3
4 vw . . . . . . . 8
54cv 1451 . . . . . . 7
6 chash 12553 . . . . . . 7
75, 6cfv 5589 . . . . . 6
8 c3 10682 . . . . . 6
97, 8wceq 1452 . . . . 5
10 cc0 9557 . . . . . . . 8
1110, 5cfv 5589 . . . . . . 7
12 c2 10681 . . . . . . . 8
1312, 5cfv 5589 . . . . . . 7
142cv 1451 . . . . . . . 8
15 cds 15277 . . . . . . . 8
1614, 15cfv 5589 . . . . . . 7
1711, 13, 16co 6308 . . . . . 6
18 c1 9558 . . . . . . . . . 10
1918, 5cfv 5589 . . . . . . . . 9
20 cmir 24776 . . . . . . . . . 10 pInvG
2114, 20cfv 5589 . . . . . . . . 9 pInvG
2219, 21cfv 5589 . . . . . . . 8 pInvG
2313, 22cfv 5589 . . . . . . 7 pInvG
2411, 23, 16co 6308 . . . . . 6 pInvG
2517, 24wceq 1452 . . . . 5 pInvG
269, 25wa 376 . . . 4 pInvG
27 cbs 15199 . . . . . 6
2814, 27cfv 5589 . . . . 5
2928cword 12703 . . . 4 Word
3026, 4, 29crab 2760 . . 3 Word pInvG
312, 3, 30cmpt 4454 . 2 Word pInvG
321, 31wceq 1452 1 ∟G Word pInvG
 Colors of variables: wff setvar class This definition is referenced by:  israg  24821
 Copyright terms: Public domain W3C validator