Metamath Proof Explorer


Theorem ltrncnvat

Description: The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013)

Ref Expression
Hypotheses ltrnel.l ˙ = K
ltrnel.a A = Atoms K
ltrnel.h H = LHyp K
ltrnel.t T = LTrn K W
Assertion ltrncnvat K HL W H F T P A F -1 P A

Proof

Step Hyp Ref Expression
1 ltrnel.l ˙ = K
2 ltrnel.a A = Atoms K
3 ltrnel.h H = LHyp K
4 ltrnel.t T = LTrn K W
5 simp3 K HL W H F T P A P A
6 eqid Base K = Base K
7 6 2 atbase P A P Base K
8 6 2 3 4 ltrncnvatb K HL W H F T P Base K P A F -1 P A
9 7 8 syl3an3 K HL W H F T P A P A F -1 P A
10 5 9 mpbid K HL W H F T P A F -1 P A