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

Definition df-angtrg 25553
Description: Select an angle in a triangle. Definition 2 of [AitkenIBCG] p. 3. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-angtrg  |- angtrg  =  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  2 ,  <" (
u `  1 )
( u `  2
) ( u ` 
3 ) "> ,  if ( x  =  3 ,  <" (
u `  2 )
( u `  3
) ( u ` 
1 ) "> , 
<" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) ) ) ) )
Distinct variable group:    u, g, x

Detailed syntax breakdown of Definition df-angtrg
StepHypRef Expression
1 cangtrg 25552 . 2  class angtrg
2 vg . . 3  set  g
3 cig 25427 . . 3  class Ig
4 vu . . . 4  set  u
5 vx . . . 4  set  x
62cv 1618 . . . . . 6  class  g
7 cpoints 25423 . . . . . 6  class PPoints
86, 7cfv 4673 . . . . 5  class  (PPoints `  g
)
9 c3 9764 . . . . 5  class  3
10 cdwords 25351 . . . . 5  class dWords
118, 9, 10co 5792 . . . 4  class  ( (PPoints `  g )dWords 3 )
12 c1 8706 . . . . 5  class  1
13 cfz 10748 . . . . 5  class  ...
1412, 9, 13co 5792 . . . 4  class  ( 1 ... 3 )
155cv 1618 . . . . . . 7  class  x
16 c2 9763 . . . . . . 7  class  2
1715, 16wceq 1619 . . . . . 6  wff  x  =  2
184cv 1618 . . . . . . . 8  class  u
1912, 18cfv 4673 . . . . . . 7  class  ( u `
 1 )
2016, 18cfv 4673 . . . . . . 7  class  ( u `
 2 )
219, 18cfv 4673 . . . . . . 7  class  ( u `
 3 )
2219, 20, 21cs3 11457 . . . . . 6  class  <" (
u `  1 )
( u `  2
) ( u ` 
3 ) ">
2315, 9wceq 1619 . . . . . . 7  wff  x  =  3
2420, 21, 19cs3 11457 . . . . . . 7  class  <" (
u `  2 )
( u `  3
) ( u ` 
1 ) ">
2521, 19, 20cs3 11457 . . . . . . 7  class  <" (
u `  3 )
( u `  1
) ( u ` 
2 ) ">
2623, 24, 25cif 3539 . . . . . 6  class  if ( x  =  3 , 
<" ( u ` 
2 ) ( u `
 3 ) ( u `  1 ) "> ,  <" ( u `  3
) ( u ` 
1 ) ( u `
 2 ) "> )
2717, 22, 26cif 3539 . . . . 5  class  if ( x  =  2 , 
<" ( u ` 
1 ) ( u `
 2 ) ( u `  3 ) "> ,  if ( x  =  3 ,  <" ( u `
 2 ) ( u `  3 ) ( u `  1
) "> ,  <" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) )
28 cangle 25524 . . . . . 6  class angle
296, 28cfv 4673 . . . . 5  class  (angle `  g )
3027, 29cfv 4673 . . . 4  class  ( (angle `  g ) `  if ( x  =  2 ,  <" ( u `
 1 ) ( u `  2 ) ( u `  3
) "> ,  if ( x  =  3 ,  <" ( u `
 2 ) ( u `  3 ) ( u `  1
) "> ,  <" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) ) )
314, 5, 11, 14, 30cmpt2 5794 . . 3  class  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  2 ,  <" (
u `  1 )
( u `  2
) ( u ` 
3 ) "> ,  if ( x  =  3 ,  <" (
u `  2 )
( u `  3
) ( u ` 
1 ) "> , 
<" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) ) ) )
322, 3, 31cmpt 4051 . 2  class  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  2 ,  <" (
u `  1 )
( u `  2
) ( u ` 
3 ) "> ,  if ( x  =  3 ,  <" (
u `  2 )
( u `  3
) ( u ` 
1 ) "> , 
<" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) ) ) ) )
331, 32wceq 1619 1  wff angtrg  =  ( g  e. Ig  |->  ( u  e.  ( (PPoints `  g
)dWords 3 ) ,  x  e.  ( 1 ... 3 )  |->  ( (angle `  g ) `  if ( x  =  2 ,  <" (
u `  1 )
( u `  2
) ( u ` 
3 ) "> ,  if ( x  =  3 ,  <" (
u `  2 )
( u `  3
) ( u ` 
1 ) "> , 
<" ( u ` 
3 ) ( u `
 1 ) ( u `  2 ) "> ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator