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

Definition df-trcng 25588
Description: Congruence of two triangles. Triangles are congruent if their sides and angles are congruent. "Technically, congruence is not a property of triangles themselves, but of triangles with a given ordering of their vertices. Triangles that are congruent under one ordering, might not be under other orderings." Definition 2 of [AitkenIBCG] p. 3. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-trcng  |- trcng  =  ( g  e.  _V  |->  {
<. u ,  v >.  |  ( ( u  e.  ( (PPoints `  g
)dWords 3 )  /\  v  e.  ( (PPoints `  g )dWords 3 ) )  /\  ( ( u (segtrg `  g
) 1 ) (segc `  g ) ( v (segtrg `  g )
1 )  /\  (
u (segtrg `  g
) 2 ) (segc `  g ) ( v (segtrg `  g )
2 )  /\  (
u (segtrg `  g
) 3 ) (segc `  g ) ( v (segtrg `  g )
3 ) )  /\  ( ( u (angtrg `  g ) 2 ) (angc `  g )
( v (angtrg `  g ) 2 )  /\  ( u (angtrg `  g ) 3 ) (angc `  g )
( v (angtrg `  g ) 3 )  /\  ( u (angtrg `  g ) 1 ) (angc `  g )
( v (angtrg `  g ) 1 ) ) ) } )
Distinct variable group:    u, g, v

Detailed syntax breakdown of Definition df-trcng
StepHypRef Expression
1 ctrcng 25560 . 2  class trcng
2 vg . . 3  set  g
3 cvv 2789 . . 3  class  _V
4 vu . . . . . . . 8  set  u
54cv 1623 . . . . . . 7  class  u
62cv 1623 . . . . . . . . 9  class  g
7 cpoints 25455 . . . . . . . . 9  class PPoints
86, 7cfv 5221 . . . . . . . 8  class  (PPoints `  g
)
9 c3 9791 . . . . . . . 8  class  3
10 cdwords 25383 . . . . . . . 8  class dWords
118, 9, 10co 5819 . . . . . . 7  class  ( (PPoints `  g )dWords 3 )
125, 11wcel 1685 . . . . . 6  wff  u  e.  ( (PPoints `  g
)dWords 3 )
13 vv . . . . . . . 8  set  v
1413cv 1623 . . . . . . 7  class  v
1514, 11wcel 1685 . . . . . 6  wff  v  e.  ( (PPoints `  g
)dWords 3 )
1612, 15wa 360 . . . . 5  wff  ( u  e.  ( (PPoints `  g
)dWords 3 )  /\  v  e.  ( (PPoints `  g )dWords 3 ) )
17 c1 8733 . . . . . . . 8  class  1
18 csegtrg 25586 . . . . . . . . 9  class segtrg
196, 18cfv 5221 . . . . . . . 8  class  (segtrg `  g )
205, 17, 19co 5819 . . . . . . 7  class  ( u (segtrg `  g )
1 )
2114, 17, 19co 5819 . . . . . . 7  class  ( v (segtrg `  g )
1 )
22 csegc 25579 . . . . . . . 8  class segc
236, 22cfv 5221 . . . . . . 7  class  (segc `  g )
2420, 21, 23wbr 4024 . . . . . 6  wff  ( u (segtrg `  g )
1 ) (segc `  g ) ( v (segtrg `  g )
1 )
25 c2 9790 . . . . . . . 8  class  2
265, 25, 19co 5819 . . . . . . 7  class  ( u (segtrg `  g )
2 )
2714, 25, 19co 5819 . . . . . . 7  class  ( v (segtrg `  g )
2 )
2826, 27, 23wbr 4024 . . . . . 6  wff  ( u (segtrg `  g )
2 ) (segc `  g ) ( v (segtrg `  g )
2 )
295, 9, 19co 5819 . . . . . . 7  class  ( u (segtrg `  g )
3 )
3014, 9, 19co 5819 . . . . . . 7  class  ( v (segtrg `  g )
3 )
3129, 30, 23wbr 4024 . . . . . 6  wff  ( u (segtrg `  g )
3 ) (segc `  g ) ( v (segtrg `  g )
3 )
3224, 28, 31w3a 936 . . . . 5  wff  ( ( u (segtrg `  g
) 1 ) (segc `  g ) ( v (segtrg `  g )
1 )  /\  (
u (segtrg `  g
) 2 ) (segc `  g ) ( v (segtrg `  g )
2 )  /\  (
u (segtrg `  g
) 3 ) (segc `  g ) ( v (segtrg `  g )
3 ) )
33 cangtrg 25584 . . . . . . . . 9  class angtrg
346, 33cfv 5221 . . . . . . . 8  class  (angtrg `  g )
355, 25, 34co 5819 . . . . . . 7  class  ( u (angtrg `  g )
2 )
3614, 25, 34co 5819 . . . . . . 7  class  ( v (angtrg `  g )
2 )
37 cangc 25582 . . . . . . . 8  class angc
386, 37cfv 5221 . . . . . . 7  class  (angc `  g )
3935, 36, 38wbr 4024 . . . . . 6  wff  ( u (angtrg `  g )
2 ) (angc `  g ) ( v (angtrg `  g )
2 )
405, 9, 34co 5819 . . . . . . 7  class  ( u (angtrg `  g )
3 )
4114, 9, 34co 5819 . . . . . . 7  class  ( v (angtrg `  g )
3 )
4240, 41, 38wbr 4024 . . . . . 6  wff  ( u (angtrg `  g )
3 ) (angc `  g ) ( v (angtrg `  g )
3 )
435, 17, 34co 5819 . . . . . . 7  class  ( u (angtrg `  g )
1 )
4414, 17, 34co 5819 . . . . . . 7  class  ( v (angtrg `  g )
1 )
4543, 44, 38wbr 4024 . . . . . 6  wff  ( u (angtrg `  g )
1 ) (angc `  g ) ( v (angtrg `  g )
1 )
4639, 42, 45w3a 936 . . . . 5  wff  ( ( u (angtrg `  g
) 2 ) (angc `  g ) ( v (angtrg `  g )
2 )  /\  (
u (angtrg `  g
) 3 ) (angc `  g ) ( v (angtrg `  g )
3 )  /\  (
u (angtrg `  g
) 1 ) (angc `  g ) ( v (angtrg `  g )
1 ) )
4716, 32, 46w3a 936 . . . 4  wff  ( ( u  e.  ( (PPoints `  g )dWords 3 )  /\  v  e.  ( (PPoints `  g )dWords 3 ) )  /\  ( ( u (segtrg `  g ) 1 ) (segc `  g )
( v (segtrg `  g ) 1 )  /\  ( u (segtrg `  g ) 2 ) (segc `  g )
( v (segtrg `  g ) 2 )  /\  ( u (segtrg `  g ) 3 ) (segc `  g )
( v (segtrg `  g ) 3 ) )  /\  ( ( u (angtrg `  g
) 2 ) (angc `  g ) ( v (angtrg `  g )
2 )  /\  (
u (angtrg `  g
) 3 ) (angc `  g ) ( v (angtrg `  g )
3 )  /\  (
u (angtrg `  g
) 1 ) (angc `  g ) ( v (angtrg `  g )
1 ) ) )
4847, 4, 13copab 4077 . . 3  class  { <. u ,  v >.  |  ( ( u  e.  ( (PPoints `  g )dWords 3 )  /\  v  e.  ( (PPoints `  g
)dWords 3 ) )  /\  ( ( u (segtrg `  g )
1 ) (segc `  g ) ( v (segtrg `  g )
1 )  /\  (
u (segtrg `  g
) 2 ) (segc `  g ) ( v (segtrg `  g )
2 )  /\  (
u (segtrg `  g
) 3 ) (segc `  g ) ( v (segtrg `  g )
3 ) )  /\  ( ( u (angtrg `  g ) 2 ) (angc `  g )
( v (angtrg `  g ) 2 )  /\  ( u (angtrg `  g ) 3 ) (angc `  g )
( v (angtrg `  g ) 3 )  /\  ( u (angtrg `  g ) 1 ) (angc `  g )
( v (angtrg `  g ) 1 ) ) ) }
492, 3, 48cmpt 4078 . 2  class  ( g  e.  _V  |->  { <. u ,  v >.  |  ( ( u  e.  ( (PPoints `  g )dWords 3 )  /\  v  e.  ( (PPoints `  g
)dWords 3 ) )  /\  ( ( u (segtrg `  g )
1 ) (segc `  g ) ( v (segtrg `  g )
1 )  /\  (
u (segtrg `  g
) 2 ) (segc `  g ) ( v (segtrg `  g )
2 )  /\  (
u (segtrg `  g
) 3 ) (segc `  g ) ( v (segtrg `  g )
3 ) )  /\  ( ( u (angtrg `  g ) 2 ) (angc `  g )
( v (angtrg `  g ) 2 )  /\  ( u (angtrg `  g ) 3 ) (angc `  g )
( v (angtrg `  g ) 3 )  /\  ( u (angtrg `  g ) 1 ) (angc `  g )
( v (angtrg `  g ) 1 ) ) ) } )
501, 49wceq 1624 1  wff trcng  =  ( g  e.  _V  |->  {
<. u ,  v >.  |  ( ( u  e.  ( (PPoints `  g
)dWords 3 )  /\  v  e.  ( (PPoints `  g )dWords 3 ) )  /\  ( ( u (segtrg `  g
) 1 ) (segc `  g ) ( v (segtrg `  g )
1 )  /\  (
u (segtrg `  g
) 2 ) (segc `  g ) ( v (segtrg `  g )
2 )  /\  (
u (segtrg `  g
) 3 ) (segc `  g ) ( v (segtrg `  g )
3 ) )  /\  ( ( u (angtrg `  g ) 2 ) (angc `  g )
( v (angtrg `  g ) 2 )  /\  ( u (angtrg `  g ) 3 ) (angc `  g )
( v (angtrg `  g ) 3 )  /\  ( u (angtrg `  g ) 1 ) (angc `  g )
( v (angtrg `  g ) 1 ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator