Metamath Proof Explorer


Theorem ltrncoelN

Description: Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel uses. (Contributed by NM, 1-May-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ltrnel.l ˙ = K
ltrnel.a A = Atoms K
ltrnel.h H = LHyp K
ltrnel.t T = LTrn K W
Assertion ltrncoelN K HL W H F T G T P A ¬ P ˙ W F G P A ¬ F G P ˙ W

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 simp1 K HL W H F T G T P A ¬ P ˙ W K HL W H
6 simp2l K HL W H F T G T P A ¬ P ˙ W F T
7 1 2 3 4 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
8 7 3adant2l K HL W H F T G T P A ¬ P ˙ W G P A ¬ G P ˙ W
9 1 2 3 4 ltrnel K HL W H F T G P A ¬ G P ˙ W F G P A ¬ F G P ˙ W
10 5 6 8 9 syl3anc K HL W H F T G T P A ¬ P ˙ W F G P A ¬ F G P ˙ W