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

Metamath Proof Explorer

Theorem ltrnat

Description: The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel uses. (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses ltrnel.l ⊢ ≤ ˙ = ≤ K
ltrnel.a ⊢ A = Atoms ⁡ K
ltrnel.h ⊢ H = LHyp ⁡ K
ltrnel.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A → F ⁡ 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 ltrnatb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ Base K → P ∈ A ↔ F ⁡ P ∈ A
9 7 8 syl3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A → P ∈ A ↔ F ⁡ P ∈ A
10 5 9 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A → F ⁡ P ∈ A