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

Definition df-segtrg 26291
Description: Select a segment in a triangle. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-segtrg  |- segtrg  =  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  1 ,  ( ( u `  1 ) ( seg `  g
) ( u ` 
2 ) ) ,  if ( x  =  2 ,  ( ( u `  2 ) ( seg `  g
) ( u ` 
3 ) ) ,  ( ( u ` 
3 ) ( seg `  g ) ( u `
 1 ) ) ) ) ) ) )
Distinct variable group:    u, g, x

Detailed syntax breakdown of Definition df-segtrg
StepHypRef Expression
1 csegtrg 26290 . 2  class segtrg
2 vg . . 3  set  g
3 cig 26163 . . 3  class Ig
4 vu . . . 4  set  u
5 vx . . . 4  set  x
62cv 1631 . . . . . 6  class  g
7 cpoints 26159 . . . . . 6  class PPoints
86, 7cfv 5271 . . . . 5  class  (PPoints `  g
)
9 c3 9812 . . . . 5  class  3
10 cdwords 26087 . . . . 5  class dWords
118, 9, 10co 5874 . . . 4  class  ( (PPoints `  g )dWords 3 )
12 c1 8754 . . . . 5  class  1
13 cfz 10798 . . . . 5  class  ...
1412, 9, 13co 5874 . . . 4  class  ( 1 ... 3 )
155cv 1631 . . . . . . 7  class  x
1615, 12wceq 1632 . . . . . 6  wff  x  =  1
174cv 1631 . . . . . . . 8  class  u
1812, 17cfv 5271 . . . . . . 7  class  ( u `
 1 )
19 c2 9811 . . . . . . . 8  class  2
2019, 17cfv 5271 . . . . . . 7  class  ( u `
 2 )
21 cseg 26233 . . . . . . . 8  class  seg
226, 21cfv 5271 . . . . . . 7  class  ( seg `  g )
2318, 20, 22co 5874 . . . . . 6  class  ( ( u `  1 ) ( seg `  g
) ( u ` 
2 ) )
2415, 19wceq 1632 . . . . . . 7  wff  x  =  2
259, 17cfv 5271 . . . . . . . 8  class  ( u `
 3 )
2620, 25, 22co 5874 . . . . . . 7  class  ( ( u `  2 ) ( seg `  g
) ( u ` 
3 ) )
2725, 18, 22co 5874 . . . . . . 7  class  ( ( u `  3 ) ( seg `  g
) ( u ` 
1 ) )
2824, 26, 27cif 3578 . . . . . 6  class  if ( x  =  2 ,  ( ( u ` 
2 ) ( seg `  g ) ( u `
 3 ) ) ,  ( ( u `
 3 ) ( seg `  g ) ( u `  1
) ) )
2916, 23, 28cif 3578 . . . . 5  class  if ( x  =  1 ,  ( ( u ` 
1 ) ( seg `  g ) ( u `
 2 ) ) ,  if ( x  =  2 ,  ( ( u `  2
) ( seg `  g
) ( u ` 
3 ) ) ,  ( ( u ` 
3 ) ( seg `  g ) ( u `
 1 ) ) ) )
30 cangle 26260 . . . . . 6  class angle
316, 30cfv 5271 . . . . 5  class  (angle `  g )
3229, 31cfv 5271 . . . 4  class  ( (angle `  g ) `  if ( x  =  1 ,  ( ( u `
 1 ) ( seg `  g ) ( u `  2
) ) ,  if ( x  =  2 ,  ( ( u `
 2 ) ( seg `  g ) ( u `  3
) ) ,  ( ( u `  3
) ( seg `  g
) ( u ` 
1 ) ) ) ) )
334, 5, 11, 14, 32cmpt2 5876 . . 3  class  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  1 ,  ( ( u `  1 ) ( seg `  g
) ( u ` 
2 ) ) ,  if ( x  =  2 ,  ( ( u `  2 ) ( seg `  g
) ( u ` 
3 ) ) ,  ( ( u ` 
3 ) ( seg `  g ) ( u `
 1 ) ) ) ) ) )
342, 3, 33cmpt 4093 . 2  class  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  1 ,  ( ( u `  1 ) ( seg `  g
) ( u ` 
2 ) ) ,  if ( x  =  2 ,  ( ( u `  2 ) ( seg `  g
) ( u ` 
3 ) ) ,  ( ( u ` 
3 ) ( seg `  g ) ( u `
 1 ) ) ) ) ) ) )
351, 34wceq 1632 1  wff segtrg  =  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  1 ,  ( ( u `  1 ) ( seg `  g
) ( u ` 
2 ) ) ,  if ( x  =  2 ,  ( ( u `  2 ) ( seg `  g
) ( u ` 
3 ) ) ,  ( ( u ` 
3 ) ( seg `  g ) ( u `
 1 ) ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator