Metamath Proof Explorer

Definition df-trnN

Description: Define set of all translations. Definition of translation in Crawley p. 111. (Contributed by NM, 4-Feb-2012)

Ref Expression
Assertion 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 } ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrnN 
 |-  Trn
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vd 
 |-  d
4 catm 
 |-  Atoms
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( Atoms ` k )
7 vf 
 |-  f
8 cdilN 
 |-  Dil
9 5 8 cfv 
 |-  ( Dil ` k )
10 3 cv 
 |-  d
11 10 9 cfv 
 |-  ( ( Dil ` k ) ` d )
12 vq 
 |-  q
13 cwpointsN 
 |-  WAtoms
14 5 13 cfv 
 |-  ( WAtoms ` k )
15 10 14 cfv 
 |-  ( ( WAtoms ` k ) ` d )
16 vr 
 |-  r
17 12 cv 
 |-  q
18 cpadd 
 |-  +P
19 5 18 cfv 
 |-  ( +P ` k )
20 7 cv 
 |-  f
21 17 20 cfv 
 |-  ( f ` q )
22 17 21 19 co 
 |-  ( q ( +P ` k ) ( f ` q ) )
23 cpolN 
 |-  _|_P
24 5 23 cfv 
 |-  ( _|_P ` k )
25 10 csn 
 |-  { d }
26 25 24 cfv 
 |-  ( ( _|_P ` k ) ` { d } )
27 22 26 cin 
 |-  ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) )
28 16 cv 
 |-  r
29 28 20 cfv 
 |-  ( f ` r )
30 28 29 19 co 
 |-  ( r ( +P ` k ) ( f ` r ) )
31 30 26 cin 
 |-  ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) )
32 27 31 wceq 
 |-  ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) )
33 32 16 15 wral 
 |-  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 } ) )
34 33 12 15 wral 
 |-  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 } ) )
35 34 7 11 crab 
 |-  { 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 } ) ) }
36 3 6 35 cmpt 
 |-  ( 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 } ) ) } )
37 1 2 36 cmpt 
 |-  ( 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 } ) ) } ) )
38 0 37 wceq 
 |-  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 } ) ) } ) )