Metamath Proof Explorer

Definition df-trl

Description: Define trace of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Assertion df-trl 
|- trL = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrl 
 |-  trL
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 cltrn 
 |-  LTrn
9 5 8 cfv 
 |-  ( LTrn ` k )
10 3 cv 
 |-  w
11 10 9 cfv 
 |-  ( ( LTrn ` k ) ` w )
12 vx 
 |-  x
13 cbs 
 |-  Base
14 5 13 cfv 
 |-  ( Base ` k )
15 vp 
 |-  p
16 catm 
 |-  Atoms
17 5 16 cfv 
 |-  ( Atoms ` k )
18 15 cv 
 |-  p
19 cple 
 |-  le
20 5 19 cfv 
 |-  ( le ` k )
21 18 10 20 wbr 
 |-  p ( le ` k ) w
22 21 wn 
 |-  -. p ( le ` k ) w
23 12 cv 
 |-  x
24 cjn 
 |-  join
25 5 24 cfv 
 |-  ( join ` k )
26 7 cv 
 |-  f
27 18 26 cfv 
 |-  ( f ` p )
28 18 27 25 co 
 |-  ( p ( join ` k ) ( f ` p ) )
29 cmee 
 |-  meet
30 5 29 cfv 
 |-  ( meet ` k )
31 28 10 30 co 
 |-  ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w )
32 23 31 wceq 
 |-  x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w )
33 22 32 wi 
 |-  ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) )
34 33 15 17 wral 
 |-  A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) )
35 34 12 14 crio 
 |-  ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) )
36 7 11 35 cmpt 
 |-  ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) )
37 3 6 36 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) ) )
38 1 2 37 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) ) ) )
39 0 38 wceq 
 |-  trL = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) ) ) )