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