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 26169
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 26168 . 2  class angle
2 vg . . 3  set  g
3 cibg 26118 . . 3  class Ibg
4 vw . . . 4  set  w
52cv 1624 . . . . . 6  class  g
6 cpoints 26067 . . . . . 6  class PPoints
75, 6cfv 5257 . . . . 5  class  (PPoints `  g
)
8 c3 9798 . . . . 5  class  3
9 cdwords 25995 . . . . 5  class dWords
107, 8, 9co 5860 . . . 4  class  ( (PPoints `  g )dWords 3 )
11 c2 9797 . . . . . . 7  class  2
124cv 1624 . . . . . . 7  class  w
1311, 12cfv 5257 . . . . . 6  class  ( w `
 2 )
14 c1 8740 . . . . . . 7  class  1
1514, 12cfv 5257 . . . . . 6  class  ( w `
 1 )
16 cray2 26162 . . . . . . 7  class ray
175, 16cfv 5257 . . . . . 6  class  (ray `  g )
1813, 15, 17co 5860 . . . . 5  class  ( ( w `  2 ) (ray `  g )
( w `  1
) )
198, 12cfv 5257 . . . . . 6  class  ( w `
 3 )
2013, 19, 17co 5860 . . . . 5  class  ( ( w `  2 ) (ray `  g )
( w `  3
) )
2118, 20cun 3152 . . . 4  class  ( ( ( w `  2
) (ray `  g
) ( w ` 
1 ) )  u.  ( ( w ` 
2 ) (ray `  g ) ( w `
 3 ) ) )
224, 10, 21cmpt 4079 . . 3  class  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( w ` 
2 ) (ray `  g ) ( w `
 1 ) )  u.  ( ( w `
 2 ) (ray
`  g ) ( w `  3 ) ) ) )
232, 3, 22cmpt 4079 . 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 1625 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