This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltrncoat

Description: Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel , ltrnat uses. (Contributed by NM, 1-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 ltrncoat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ⁡ G ⁡ 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 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → K ∈ HL ∧ W ∈ H
6 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ∈ T
7 1 2 3 4 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A → G ⁡ P ∈ A
8 7 3adant2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → G ⁡ P ∈ A
9 1 2 3 4 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A → F ⁡ G ⁡ P ∈ A
10 5 6 8 9 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ⁡ G ⁡ P ∈ A