MPE Home 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  =  ( g  e.  _V  |->  { w  e. Word  ( Base `  g )  |  ( ( # `  w
)  =  3  /\  ( ( w ` 
0 ) ( dist `  g ) ( w `
 2 ) )  =  ( ( w `
 0 ) (
dist `  g )
( ( (pInvG `  g ) `  (
w `  1 )
) `  ( w `  2 ) ) ) ) } )
Distinct variable group:    w, g

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