This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ltrn

Description: Define set of all lattice translations. Similar to definition of translation in Crawley p. 111. (Contributed by NM, 11-May-2012)

Ref Expression
Assertion df-ltrn 
|- LTrn = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrn 
 |-  LTrn
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vf 
 |-  f
8 cldil 
 |-  LDil
9 5 8 cfv 
 |-  ( LDil ` k )
10 3 cv 
 |-  w
11 10 9 cfv 
 |-  ( ( LDil ` k ) ` w )
12 vp 
 |-  p
13 catm 
 |-  Atoms
14 5 13 cfv 
 |-  ( Atoms ` k )
15 vq 
 |-  q
16 12 cv 
 |-  p
17 cple 
 |-  le
18 5 17 cfv 
 |-  ( le ` k )
19 16 10 18 wbr 
 |-  p ( le ` k ) w
20 19 wn 
 |-  -. p ( le ` k ) w
21 15 cv 
 |-  q
22 21 10 18 wbr 
 |-  q ( le ` k ) w
23 22 wn 
 |-  -. q ( le ` k ) w
24 20 23 wa 
 |-  ( -. p ( le ` k ) w /\ -. q ( le ` k ) w )
25 cjn 
 |-  join
26 5 25 cfv 
 |-  ( join ` k )
27 7 cv 
 |-  f
28 16 27 cfv 
 |-  ( f ` p )
29 16 28 26 co 
 |-  ( p ( join ` k ) ( f ` p ) )
30 cmee 
 |-  meet
31 5 30 cfv 
 |-  ( meet ` k )
32 29 10 31 co 
 |-  ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w )
33 21 27 cfv 
 |-  ( f ` q )
34 21 33 26 co 
 |-  ( q ( join ` k ) ( f ` q ) )
35 34 10 31 co 
 |-  ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w )
36 32 35 wceq 
 |-  ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w )
37 24 36 wi 
 |-  ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) )
38 37 15 14 wral 
 |-  A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) )
39 38 12 14 wral 
 |-  A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) )
40 39 7 11 crab 
 |-  { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) }
41 3 6 40 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) } )
42 1 2 41 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) } ) )
43 0 42 wceq 
 |-  LTrn = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) } ) )