Metamath Proof Explorer

Theorem ltrncnvatb

Description: The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012)

Ref Expression
Hypotheses ltrnatb.b ⊢ B = Base K
ltrnatb.a ⊢ A = Atoms ⁡ K
ltrnatb.h ⊢ H = LHyp ⁡ K
ltrnatb.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrncnvatb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → P ∈ A ↔ F -1 ⁡ P ∈ A

Proof

Step Hyp Ref Expression
1 ltrnatb.b ⊢ B = Base K
2 ltrnatb.a ⊢ A = Atoms ⁡ K
3 ltrnatb.h ⊢ H = LHyp ⁡ K
4 ltrnatb.t ⊢ T = LTrn ⁡ K ⁡ W
5 1 3 4 ltrn1o ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F : B ⟶ 1-1 onto B
6 f1ocnvdm ⊢ F : B ⟶ 1-1 onto B ∧ P ∈ B → F -1 ⁡ P ∈ B
7 5 6 stoic3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → F -1 ⁡ P ∈ B
8 1 2 3 4 ltrnatb ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F -1 ⁡ P ∈ B → F -1 ⁡ P ∈ A ↔ F ⁡ F -1 ⁡ P ∈ A
9 7 8 syld3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → F -1 ⁡ P ∈ A ↔ F ⁡ F -1 ⁡ P ∈ A
10 f1ocnvfv2 ⊢ F : B ⟶ 1-1 onto B ∧ P ∈ B → F ⁡ F -1 ⁡ P = P
11 5 10 stoic3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → F ⁡ F -1 ⁡ P = P
12 11 eleq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → F ⁡ F -1 ⁡ P ∈ A ↔ P ∈ A
13 9 12 bitr2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ B → P ∈ A ↔ F -1 ⁡ P ∈ A