Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tgrp Unicode version

Definition df-tgrp 29621
Description: Define the class of all translation groups.  k is normally a member of  HL. Each base set is the set of all lattice translations with respect to a hyperplane  w, and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.)
Assertion
Ref Expression
df-tgrp  |-  TGrp  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  {
<. ( Base `  ndx ) ,  ( ( LTrn `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. } ) )
Distinct variable group:    w, k, f, g

Detailed syntax breakdown of Definition df-tgrp
StepHypRef Expression
1 ctgrp 29620 . 2  class  TGrp
2 vk . . 3  set  k
3 cvv 2727 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1618 . . . . 5  class  k
6 clh 28862 . . . . 5  class  LHyp
75, 6cfv 4592 . . . 4  class  ( LHyp `  k )
8 cnx 13019 . . . . . . 7  class  ndx
9 cbs 13022 . . . . . . 7  class  Base
108, 9cfv 4592 . . . . . 6  class  ( Base `  ndx )
114cv 1618 . . . . . . 7  class  w
12 cltrn 28979 . . . . . . . 8  class  LTrn
135, 12cfv 4592 . . . . . . 7  class  ( LTrn `  k )
1411, 13cfv 4592 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1510, 14cop 3547 . . . . 5  class  <. ( Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >.
16 cplusg 13082 . . . . . . 7  class  +g
178, 16cfv 4592 . . . . . 6  class  ( +g  ` 
ndx )
18 vf . . . . . . 7  set  f
19 vg . . . . . . 7  set  g
2018cv 1618 . . . . . . . 8  class  f
2119cv 1618 . . . . . . . 8  class  g
2220, 21ccom 4584 . . . . . . 7  class  ( f  o.  g )
2318, 19, 14, 14, 22cmpt2 5712 . . . . . 6  class  ( f  e.  ( ( LTrn `  k ) `  w
) ,  g  e.  ( ( LTrn `  k
) `  w )  |->  ( f  o.  g
) )
2417, 23cop 3547 . . . . 5  class  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>.
2515, 24cpr 3545 . . . 4  class  { <. (
Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. }
264, 7, 25cmpt 3974 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { <. ( Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. } )
272, 3, 26cmpt 3974 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { <. ( Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. } ) )
281, 27wceq 1619 1  wff  TGrp  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  {
<. ( Base `  ndx ) ,  ( ( LTrn `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. } ) )
Colors of variables: wff set class
This definition is referenced by:  tgrpfset  29622
  Copyright terms: Public domain W3C validator