Metamath Proof Explorer

Theorem ltrnset

Description: The set of lattice translations for a fiducial co-atom W . (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 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 ) ) } )

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 ltrnfset 
 |-  ( K e. B -> ( 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 ) ) } ) )
9 8 fveq1d 
 |-  ( K e. B -> ( ( LTrn ` 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 ) ) } ) ` W ) )
10 7 9 eqtrid 
 |-  ( K e. B -> T = ( ( 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 ) ) } ) ` W ) )
11 fveq2 
 |-  ( w = W -> ( ( LDil ` K ) ` w ) = ( ( LDil ` K ) ` W ) )
12 11 6 eqtr4di 
 |-  ( w = W -> ( ( LDil ` K ) ` w ) = D )
13 breq2 
 |-  ( w = W -> ( p .<_ w <-> p .<_ W ) )
14 13 notbid 
 |-  ( w = W -> ( -. p .<_ w <-> -. p .<_ W ) )
15 breq2 
 |-  ( w = W -> ( q .<_ w <-> q .<_ W ) )
16 15 notbid 
 |-  ( w = W -> ( -. q .<_ w <-> -. q .<_ W ) )
17 14 16 anbi12d 
 |-  ( w = W -> ( ( -. p .<_ w /\ -. q .<_ w ) <-> ( -. p .<_ W /\ -. q .<_ W ) ) )
18 oveq2 
 |-  ( w = W -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( p .\/ ( f ` p ) ) ./\ W ) )
19 oveq2 
 |-  ( w = W -> ( ( q .\/ ( f ` q ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ W ) )
20 18 19 eqeq12d 
 |-  ( w = W -> ( ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) <-> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) )
21 17 20 imbi12d 
 |-  ( w = W -> ( ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) <-> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) ) )
22 21 2ralbidv 
 |-  ( w = W -> ( 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 ) ) ) )
23 12 22 rabeqbidv 
 |-  ( w = 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 ) ) } = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } )
24 eqid 
 |-  ( 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 ) ) } ) = ( 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 ) ) } )
25 6 fvexi 
 |-  D e. _V
26 25 rabex 
 |-  { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } e. _V
27 23 24 26 fvmpt 
 |-  ( W e. H -> ( ( 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 ) ) } ) ` W ) = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } )
28 10 27 sylan9eq 
 |-  ( ( 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 ) ) } )