Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-angle Unicode version

Definition df-angle 25490
Description: Definition of an angle. Definition 17 of [AitkenIBG] p. 10. The angles can't be degenerated. Contrary to the concept of degenerated line or segment, the concept of degenerated angle no longer simplifies the wording. (For my private use only. Don't use.) (Contributed by FL, 7-Apr-2016.)
Assertion
Ref Expression
df-angle  |- angle  =  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( w ` 
2 ) (ray `  g ) ( w `
 1 ) )  u.  ( ( w `
 2 ) (ray
`  g ) ( w `  3 ) ) ) ) )
Distinct variable group:    w, g

Detailed syntax breakdown of Definition df-angle
StepHypRef Expression
1 cangle 25489 . 2  class angle
2 vg . . 3  set  g
3 cibg 25439 . . 3  class Ibg
4 vw . . . 4  set  w
52cv 1618 . . . . . 6  class  g
6 cpoints 25388 . . . . . 6  class PPoints
75, 6cfv 4638 . . . . 5  class  (PPoints `  g
)
8 c3 9729 . . . . 5  class  3
9 cdwords 25316 . . . . 5  class dWords
107, 8, 9co 5757 . . . 4  class  ( (PPoints `  g )dWords 3 )
11 c2 9728 . . . . . . 7  class  2
124cv 1618 . . . . . . 7  class  w
1311, 12cfv 4638 . . . . . 6  class  ( w `
 2 )
14 c1 8671 . . . . . . 7  class  1
1514, 12cfv 4638 . . . . . 6  class  ( w `
 1 )
16 cray2 25483 . . . . . . 7  class ray
175, 16cfv 4638 . . . . . 6  class  (ray `  g )
1813, 15, 17co 5757 . . . . 5  class  ( ( w `  2 ) (ray `  g )
( w `  1
) )
198, 12cfv 4638 . . . . . 6  class  ( w `
 3 )
2013, 19, 17co 5757 . . . . 5  class  ( ( w `  2 ) (ray `  g )
( w `  3
) )
2118, 20cun 3092 . . . 4  class  ( ( ( w `  2
) (ray `  g
) ( w ` 
1 ) )  u.  ( ( w ` 
2 ) (ray `  g ) ( w `
 3 ) ) )
224, 10, 21cmpt 4017 . . 3  class  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( w ` 
2 ) (ray `  g ) ( w `
 1 ) )  u.  ( ( w `
 2 ) (ray
`  g ) ( w `  3 ) ) ) )
232, 3, 22cmpt 4017 . 2  class  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( w ` 
2 ) (ray `  g ) ( w `
 1 ) )  u.  ( ( w `
 2 ) (ray
`  g ) ( w `  3 ) ) ) ) )
241, 23wceq 1619 1  wff angle  =  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( w ` 
2 ) (ray `  g ) ( w `
 1 ) )  u.  ( ( w `
 2 ) (ray
`  g ) ( w `  3 ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator