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

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