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

Definition df-trnN 30296
Description: Define set of all translations. Definition of translation in [Crawley] p. 111. (Contributed by NM, 4-Feb-2012.)
Assertion
Ref Expression
df-trnN  |-  Trn  =  ( k  e.  _V  |->  ( d  e.  (
Atoms `  k )  |->  { f  e.  ( ( Dil `  k ) `
 d )  | 
A. q  e.  ( ( WAtoms `  k ) `  d ) A. r  e.  ( ( WAtoms `  k
) `  d )
( ( q ( + P `  k
) ( f `  q ) )  i^i  ( ( _|_ P `  k ) `  {
d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) ) } ) )
Distinct variable group:    k, d, f, q, r

Detailed syntax breakdown of Definition df-trnN
StepHypRef Expression
1 ctrnN 30292 . 2  class  Trn
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vd . . . 4  set  d
52cv 1622 . . . . 5  class  k
6 catm 29453 . . . . 5  class  Atoms
75, 6cfv 5255 . . . 4  class  ( Atoms `  k )
8 vq . . . . . . . . . . 11  set  q
98cv 1622 . . . . . . . . . 10  class  q
10 vf . . . . . . . . . . . 12  set  f
1110cv 1622 . . . . . . . . . . 11  class  f
129, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 q )
13 cpadd 29984 . . . . . . . . . . 11  class  + P
145, 13cfv 5255 . . . . . . . . . 10  class  ( + P `  k )
159, 12, 14co 5858 . . . . . . . . 9  class  ( q ( + P `  k ) ( f `
 q ) )
164cv 1622 . . . . . . . . . . 11  class  d
1716csn 3640 . . . . . . . . . 10  class  { d }
18 cpolN 30091 . . . . . . . . . . 11  class  _|_ P
195, 18cfv 5255 . . . . . . . . . 10  class  ( _|_
P `  k )
2017, 19cfv 5255 . . . . . . . . 9  class  ( ( _|_ P `  k
) `  { d } )
2115, 20cin 3151 . . . . . . . 8  class  ( ( q ( + P `  k ) ( f `
 q ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )
22 vr . . . . . . . . . . 11  set  r
2322cv 1622 . . . . . . . . . 10  class  r
2423, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 r )
2523, 24, 14co 5858 . . . . . . . . 9  class  ( r ( + P `  k ) ( f `
 r ) )
2625, 20cin 3151 . . . . . . . 8  class  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )
2721, 26wceq 1623 . . . . . . 7  wff  ( ( q ( + P `  k ) ( f `
 q ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )
28 cwpointsN 30175 . . . . . . . . 9  class  WAtoms
295, 28cfv 5255 . . . . . . . 8  class  ( WAtoms `  k )
3016, 29cfv 5255 . . . . . . 7  class  ( (
WAtoms `  k ) `  d )
3127, 22, 30wral 2543 . . . . . 6  wff  A. r  e.  ( ( WAtoms `  k
) `  d )
( ( q ( + P `  k
) ( f `  q ) )  i^i  ( ( _|_ P `  k ) `  {
d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )
3231, 8, 30wral 2543 . . . . 5  wff  A. q  e.  ( ( WAtoms `  k
) `  d ) A. r  e.  (
( WAtoms `  k ) `  d ) ( ( q ( + P `  k ) ( f `
 q ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )
33 cdilN 30291 . . . . . . 7  class  Dil
345, 33cfv 5255 . . . . . 6  class  ( Dil `  k )
3516, 34cfv 5255 . . . . 5  class  ( ( Dil `  k ) `
 d )
3632, 10, 35crab 2547 . . . 4  class  { f  e.  ( ( Dil `  k ) `  d
)  |  A. q  e.  ( ( WAtoms `  k
) `  d ) A. r  e.  (
( WAtoms `  k ) `  d ) ( ( q ( + P `  k ) ( f `
 q ) )  i^i  ( ( _|_
P `  k ) `  { d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) ) }
374, 7, 36cmpt 4077 . . 3  class  ( d  e.  ( Atoms `  k
)  |->  { f  e.  ( ( Dil `  k
) `  d )  |  A. q  e.  ( ( WAtoms `  k ) `  d ) A. r  e.  ( ( WAtoms `  k
) `  d )
( ( q ( + P `  k
) ( f `  q ) )  i^i  ( ( _|_ P `  k ) `  {
d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) ) } )
382, 3, 37cmpt 4077 . 2  class  ( k  e.  _V  |->  ( d  e.  ( Atoms `  k
)  |->  { f  e.  ( ( Dil `  k
) `  d )  |  A. q  e.  ( ( WAtoms `  k ) `  d ) A. r  e.  ( ( WAtoms `  k
) `  d )
( ( q ( + P `  k
) ( f `  q ) )  i^i  ( ( _|_ P `  k ) `  {
d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) ) } ) )
391, 38wceq 1623 1  wff  Trn  =  ( k  e.  _V  |->  ( d  e.  (
Atoms `  k )  |->  { f  e.  ( ( Dil `  k ) `
 d )  | 
A. q  e.  ( ( WAtoms `  k ) `  d ) A. r  e.  ( ( WAtoms `  k
) `  d )
( ( q ( + P `  k
) ( f `  q ) )  i^i  ( ( _|_ P `  k ) `  {
d } ) )  =  ( ( r ( + P `  k ) ( f `
 r ) )  i^i  ( ( _|_
P `  k ) `  { d } ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  trnfsetN  30344
  Copyright terms: Public domain W3C validator