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

Definition df-triangle 25326
Description: Definition of a triangle, degenerated or not. Definition 23 of [AitkenIBG] p. 15. (For my private use only. Don't use.) (Contributed by FL, 7-Apr-2016.)
Assertion
Ref Expression
df-triangle  |- triangle  =  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( ( w `
 1 ) ( seg `  g ) ( w `  2
) )  u.  (
( w `  2
) ( seg `  g
) ( w ` 
3 ) ) )  u.  ( ( w `
 3 ) ( seg `  g ) ( w `  1
) ) ) ) )
Distinct variable group:    w, g

Detailed syntax breakdown of Definition df-triangle
StepHypRef Expression
1 ctriangle 25325 . 2  class triangle
2 vg . . 3  set  g
3 cibg 25273 . . 3  class Ibg
4 vw . . . 4  set  w
52cv 1618 . . . . . 6  class  g
6 cpoints 25222 . . . . . 6  class PPoints
75, 6cfv 4592 . . . . 5  class  (PPoints `  g
)
8 c3 9676 . . . . 5  class  3
9 cdwords 25150 . . . . 5  class dWords
107, 8, 9co 5710 . . . 4  class  ( (PPoints `  g )dWords 3 )
11 c1 8618 . . . . . . . 8  class  1
124cv 1618 . . . . . . . 8  class  w
1311, 12cfv 4592 . . . . . . 7  class  ( w `
 1 )
14 c2 9675 . . . . . . . 8  class  2
1514, 12cfv 4592 . . . . . . 7  class  ( w `
 2 )
16 cseg 25296 . . . . . . . 8  class  seg
175, 16cfv 4592 . . . . . . 7  class  ( seg `  g )
1813, 15, 17co 5710 . . . . . 6  class  ( ( w `  1 ) ( seg `  g
) ( w ` 
2 ) )
198, 12cfv 4592 . . . . . . 7  class  ( w `
 3 )
2015, 19, 17co 5710 . . . . . 6  class  ( ( w `  2 ) ( seg `  g
) ( w ` 
3 ) )
2118, 20cun 3076 . . . . 5  class  ( ( ( w `  1
) ( seg `  g
) ( w ` 
2 ) )  u.  ( ( w ` 
2 ) ( seg `  g ) ( w `
 3 ) ) )
2219, 13, 17co 5710 . . . . 5  class  ( ( w `  3 ) ( seg `  g
) ( w ` 
1 ) )
2321, 22cun 3076 . . . 4  class  ( ( ( ( w ` 
1 ) ( seg `  g ) ( w `
 2 ) )  u.  ( ( w `
 2 ) ( seg `  g ) ( w `  3
) ) )  u.  ( ( w ` 
3 ) ( seg `  g ) ( w `
 1 ) ) )
244, 10, 23cmpt 3974 . . 3  class  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( ( w `
 1 ) ( seg `  g ) ( w `  2
) )  u.  (
( w `  2
) ( seg `  g
) ( w ` 
3 ) ) )  u.  ( ( w `
 3 ) ( seg `  g ) ( w `  1
) ) ) )
252, 3, 24cmpt 3974 . 2  class  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( ( w `
 1 ) ( seg `  g ) ( w `  2
) )  u.  (
( w `  2
) ( seg `  g
) ( w ` 
3 ) ) )  u.  ( ( w `
 3 ) ( seg `  g ) ( w `  1
) ) ) ) )
261, 25wceq 1619 1  wff triangle  =  ( g  e. Ibg  |->  ( w  e.  ( (PPoints `  g
)dWords 3 )  |->  ( ( ( ( w `
 1 ) ( seg `  g ) ( w `  2
) )  u.  (
( w `  2
) ( seg `  g
) ( w ` 
3 ) ) )  u.  ( ( w `
 3 ) ( seg `  g ) ( w `  1
) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator