Metamath Proof Explorer

Theorem isltrn

Description: The predicate "is a lattice translation". Similar to definition of translation in Crawley p. 111. (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 )
ltrnset.d 
|- D = ( ( LDil ` K ) ` W )
ltrnset.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion isltrn 
|- ( ( K e. B /\ W e. H ) -> ( F e. T <-> ( F e. D /\ 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 ltrnset.d 
 |-  D = ( ( LDil ` K ) ` W )
7 ltrnset.t 
 |-  T = ( ( LTrn ` K ) ` W )
8 1 2 3 4 5 6 7 ltrnset 
 |-  ( ( K e. B /\ W e. H ) -> T = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } )
9 8 eleq2d 
 |-  ( ( K e. B /\ W e. H ) -> ( F e. T <-> F e. { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } ) )
10 fveq1 
 |-  ( f = F -> ( f ` p ) = ( F ` p ) )
11 10 oveq2d 
 |-  ( f = F -> ( p .\/ ( f ` p ) ) = ( p .\/ ( F ` p ) ) )
12 11 oveq1d 
 |-  ( f = F -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( p .\/ ( F ` p ) ) ./\ W ) )
13 fveq1 
 |-  ( f = F -> ( f ` q ) = ( F ` q ) )
14 13 oveq2d 
 |-  ( f = F -> ( q .\/ ( f ` q ) ) = ( q .\/ ( F ` q ) ) )
15 14 oveq1d 
 |-  ( f = F -> ( ( q .\/ ( f ` q ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) )
16 12 15 eqeq12d 
 |-  ( f = F -> ( ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) <-> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
17 16 imbi2d 
 |-  ( f = F -> ( ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) <-> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
18 17 2ralbidv 
 |-  ( f = F -> ( A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) <-> A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
19 18 elrab 
 |-  ( F e. { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } <-> ( F e. D /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
20 9 19 bitrdi 
 |-  ( ( K e. B /\ W e. H ) -> ( F e. T <-> ( F e. D /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )