Metamath Proof Explorer


Theorem trlfset

Description: The set of all traces of lattice translations for a lattice K . (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses trlset.b
|- B = ( Base ` K )
trlset.l
|- .<_ = ( le ` K )
trlset.j
|- .\/ = ( join ` K )
trlset.m
|- ./\ = ( meet ` K )
trlset.a
|- A = ( Atoms ` K )
trlset.h
|- H = ( LHyp ` K )
Assertion trlfset
|- ( K e. C -> ( trL ` K ) = ( w e. H |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 trlset.b
 |-  B = ( Base ` K )
2 trlset.l
 |-  .<_ = ( le ` K )
3 trlset.j
 |-  .\/ = ( join ` K )
4 trlset.m
 |-  ./\ = ( meet ` K )
5 trlset.a
 |-  A = ( Atoms ` K )
6 trlset.h
 |-  H = ( LHyp ` K )
7 elex
 |-  ( K e. C -> K e. _V )
8 fveq2
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
9 8 6 eqtr4di
 |-  ( k = K -> ( LHyp ` k ) = H )
10 fveq2
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
11 10 fveq1d
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
12 fveq2
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
13 12 1 eqtr4di
 |-  ( k = K -> ( Base ` k ) = B )
14 fveq2
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
15 14 5 eqtr4di
 |-  ( k = K -> ( Atoms ` k ) = A )
16 fveq2
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
17 16 2 eqtr4di
 |-  ( k = K -> ( le ` k ) = .<_ )
18 17 breqd
 |-  ( k = K -> ( p ( le ` k ) w <-> p .<_ w ) )
19 18 notbid
 |-  ( k = K -> ( -. p ( le ` k ) w <-> -. p .<_ w ) )
20 fveq2
 |-  ( k = K -> ( meet ` k ) = ( meet ` K ) )
21 20 4 eqtr4di
 |-  ( k = K -> ( meet ` k ) = ./\ )
22 fveq2
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
23 22 3 eqtr4di
 |-  ( k = K -> ( join ` k ) = .\/ )
24 23 oveqd
 |-  ( k = K -> ( p ( join ` k ) ( f ` p ) ) = ( p .\/ ( f ` p ) ) )
25 eqidd
 |-  ( k = K -> w = w )
26 21 24 25 oveq123d
 |-  ( k = K -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( p .\/ ( f ` p ) ) ./\ w ) )
27 26 eqeq2d
 |-  ( k = K -> ( x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) <-> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) )
28 19 27 imbi12d
 |-  ( k = K -> ( ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) <-> ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) )
29 15 28 raleqbidv
 |-  ( k = K -> ( A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) <-> A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) )
30 13 29 riotaeqbidv
 |-  ( k = K -> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) = ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) )
31 11 30 mpteq12dv
 |-  ( k = 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 ) ) ) ) = ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) )
32 9 31 mpteq12dv
 |-  ( k = K -> ( 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 ) ) ) ) ) = ( w e. H |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) ) )
33 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 ) ) ) ) ) )
34 32 33 6 mptfvmpt
 |-  ( K e. _V -> ( trL ` K ) = ( w e. H |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) ) )
35 7 34 syl
 |-  ( K e. C -> ( trL ` K ) = ( w e. H |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) ) )