Metamath Proof Explorer


Theorem idltrn

Description: The identity function is a lattice translation. Remark below Lemma B in Crawley p. 112. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses idltrn.b B=BaseK
idltrn.h H=LHypK
idltrn.t T=LTrnKW
Assertion idltrn KHLWHIBT

Proof

Step Hyp Ref Expression
1 idltrn.b B=BaseK
2 idltrn.h H=LHypK
3 idltrn.t T=LTrnKW
4 eqid LDilKW=LDilKW
5 1 2 4 idldil KHLWHIBLDilKW
6 simpll KHLWHpAtomsKqAtomsK¬pKW¬qKWKHLWH
7 simplrr KHLWHpAtomsKqAtomsK¬pKW¬qKWqAtomsK
8 simprr KHLWHpAtomsKqAtomsK¬pKW¬qKW¬qKW
9 eqid K=K
10 eqid meetK=meetK
11 eqid 0.K=0.K
12 eqid AtomsK=AtomsK
13 9 10 11 12 2 lhpmat KHLWHqAtomsK¬qKWqmeetKW=0.K
14 6 7 8 13 syl12anc KHLWHpAtomsKqAtomsK¬pKW¬qKWqmeetKW=0.K
15 1 12 atbase qAtomsKqB
16 fvresi qBIBq=q
17 7 15 16 3syl KHLWHpAtomsKqAtomsK¬pKW¬qKWIBq=q
18 17 oveq2d KHLWHpAtomsKqAtomsK¬pKW¬qKWqjoinKIBq=qjoinKq
19 simplll KHLWHpAtomsKqAtomsK¬pKW¬qKWKHL
20 eqid joinK=joinK
21 20 12 hlatjidm KHLqAtomsKqjoinKq=q
22 19 7 21 syl2anc KHLWHpAtomsKqAtomsK¬pKW¬qKWqjoinKq=q
23 18 22 eqtrd KHLWHpAtomsKqAtomsK¬pKW¬qKWqjoinKIBq=q
24 23 oveq1d KHLWHpAtomsKqAtomsK¬pKW¬qKWqjoinKIBqmeetKW=qmeetKW
25 simplrl KHLWHpAtomsKqAtomsK¬pKW¬qKWpAtomsK
26 1 12 atbase pAtomsKpB
27 fvresi pBIBp=p
28 25 26 27 3syl KHLWHpAtomsKqAtomsK¬pKW¬qKWIBp=p
29 28 oveq2d KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBp=pjoinKp
30 20 12 hlatjidm KHLpAtomsKpjoinKp=p
31 19 25 30 syl2anc KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKp=p
32 29 31 eqtrd KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBp=p
33 32 oveq1d KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=pmeetKW
34 simprl KHLWHpAtomsKqAtomsK¬pKW¬qKW¬pKW
35 9 10 11 12 2 lhpmat KHLWHpAtomsK¬pKWpmeetKW=0.K
36 6 25 34 35 syl12anc KHLWHpAtomsKqAtomsK¬pKW¬qKWpmeetKW=0.K
37 33 36 eqtrd KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=0.K
38 14 24 37 3eqtr4rd KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=qjoinKIBqmeetKW
39 38 ex KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=qjoinKIBqmeetKW
40 39 ralrimivva KHLWHpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=qjoinKIBqmeetKW
41 9 20 10 12 2 4 3 isltrn KHLWHIBTIBLDilKWpAtomsKqAtomsK¬pKW¬qKWpjoinKIBpmeetKW=qjoinKIBqmeetKW
42 5 40 41 mpbir2and KHLWHIBT