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