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 ˙ = 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 B W H F T F D p A q A ¬ p ˙ W ¬ q ˙ W 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 ltrnset K B W H T = f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W
9 8 eleq2d K B W H F T F f D | p A q 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 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 ˙ F p ˙ W = q ˙ F q ˙ W
19 18 elrab F 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 ˙ F p ˙ W = q ˙ F q ˙ W
20 9 19 bitrdi K B W H F T F D p A q A ¬ p ˙ W ¬ q ˙ W p ˙ F p ˙ W = q ˙ F q ˙ W