Metamath Proof Explorer

Theorem isltrn2N

Description: The predicate "is a lattice translation". Version of isltrn that considers only different p and q . TODO: Can this eliminate some separate proofs for the p = q case? (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

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 isltrn2N 
|- ( ( 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 =/= q ) -> ( ( 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 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 ) ) ) ) )
9 3simpa 
 |-  ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( -. p .<_ W /\ -. q .<_ W ) )
10 9 imim1i 
 |-  ( ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) -> ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
11 3anass 
 |-  ( ( p =/= q /\ -. p .<_ W /\ -. q .<_ W ) <-> ( p =/= q /\ ( -. p .<_ W /\ -. q .<_ W ) ) )
12 3anrot 
 |-  ( ( p =/= q /\ -. p .<_ W /\ -. q .<_ W ) <-> ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) )
13 df-ne 
 |-  ( p =/= q <-> -. p = q )
14 13 anbi1i 
 |-  ( ( p =/= q /\ ( -. p .<_ W /\ -. q .<_ W ) ) <-> ( -. p = q /\ ( -. p .<_ W /\ -. q .<_ W ) ) )
15 11 12 14 3bitr3i 
 |-  ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) <-> ( -. p = q /\ ( -. p .<_ W /\ -. q .<_ W ) ) )
16 15 imbi1i 
 |-  ( ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( ( -. p = q /\ ( -. p .<_ W /\ -. q .<_ W ) ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
17 impexp 
 |-  ( ( ( -. p = q /\ ( -. p .<_ W /\ -. q .<_ W ) ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( -. p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
18 16 17 bitri 
 |-  ( ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( -. p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
19 id 
 |-  ( p = q -> p = q )
20 fveq2 
 |-  ( p = q -> ( F ` p ) = ( F ` q ) )
21 19 20 oveq12d 
 |-  ( p = q -> ( p .\/ ( F ` p ) ) = ( q .\/ ( F ` q ) ) )
22 21 oveq1d 
 |-  ( p = q -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) )
23 22 a1d 
 |-  ( p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
24 pm2.61 
 |-  ( ( p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) -> ( ( -. p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
25 23 24 ax-mp 
 |-  ( ( -. p = q -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
26 18 25 sylbi 
 |-  ( ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) -> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
27 10 26 impbii 
 |-  ( ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) <-> ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
28 27 2ralbii 
 |-  ( 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 =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) )
29 28 anbi2i 
 |-  ( ( 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 =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) )
30 8 29 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 =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )