Metamath Proof Explorer

Theorem ltrnfset

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

Ref Expression
Hypotheses ltrnset.l 
|- .<_ = ( le ` K )
ltrnset.j 
|- .\/ = ( join ` K )
ltrnset.m 
|- ./\ = ( meet ` K )
ltrnset.a 
|- A = ( Atoms ` K )
ltrnset.h 
|- H = ( LHyp ` K )
Assertion ltrnfset 
|- ( K e. C -> ( LTrn ` K ) = ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) )

Proof

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