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 } ) ) } ) )