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 ˙ = 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 B W H F T F D p A q A ¬ p ˙ W ¬ q ˙ W p q p ˙ F p ˙ W = q ˙ F q ˙ W

Proof

Step Hyp Ref Expression
1 ltrnset.l ˙ = 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 B W H F T F D p A q 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 p A q A ¬ p ˙ W ¬ q ˙ W p ˙ F p ˙ W = q ˙ F q ˙ W p A q A ¬ p ˙ W ¬ q ˙ W p q p ˙ F p ˙ W = q ˙ F q ˙ W
29 28 anbi2i F D p A q A ¬ p ˙ W ¬ q ˙ W p ˙ F p ˙ W = q ˙ F q ˙ W F D p A q A ¬ p ˙ W ¬ q ˙ W p q p ˙ F p ˙ W = q ˙ F q ˙ W
30 8 29 bitrdi K B W H F T F D p A q A ¬ p ˙ W ¬ q ˙ W p q p ˙ F p ˙ W = q ˙ F q ˙ W