# 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}={\mathrm{Base}}_{{K}}$
ltrnatb.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
ltrnatb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
ltrnatb.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion ltrncnvatb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to \left({P}\in {A}↔{{F}}^{-1}\left({P}\right)\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 ltrnatb.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 ltrnatb.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 ltrnatb.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 ltrnatb.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 1 3 4 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
6 f1ocnvdm ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {P}\in {B}\right)\to {{F}}^{-1}\left({P}\right)\in {B}$
7 5 6 stoic3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to {{F}}^{-1}\left({P}\right)\in {B}$
8 1 2 3 4 ltrnatb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {{F}}^{-1}\left({P}\right)\in {B}\right)\to \left({{F}}^{-1}\left({P}\right)\in {A}↔{F}\left({{F}}^{-1}\left({P}\right)\right)\in {A}\right)$
9 7 8 syld3an3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to \left({{F}}^{-1}\left({P}\right)\in {A}↔{F}\left({{F}}^{-1}\left({P}\right)\right)\in {A}\right)$
10 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {P}\in {B}\right)\to {F}\left({{F}}^{-1}\left({P}\right)\right)={P}$
11 5 10 stoic3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to {F}\left({{F}}^{-1}\left({P}\right)\right)={P}$
12 11 eleq1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to \left({F}\left({{F}}^{-1}\left({P}\right)\right)\in {A}↔{P}\in {A}\right)$
13 9 12 bitr2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {P}\in {B}\right)\to \left({P}\in {A}↔{{F}}^{-1}\left({P}\right)\in {A}\right)$