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 e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( `' F ` P ) e. 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 e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B )
6 f1ocnvdm
 |-  ( ( F : B -1-1-onto-> B /\ P e. B ) -> ( `' F ` P ) e. B )
7 5 6 stoic3
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( `' F ` P ) e. B )
8 1 2 3 4 ltrnatb
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( `' F ` P ) e. B ) -> ( ( `' F ` P ) e. A <-> ( F ` ( `' F ` P ) ) e. A ) )
9 7 8 syld3an3
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( `' F ` P ) e. A <-> ( F ` ( `' F ` P ) ) e. A ) )
10 f1ocnvfv2
 |-  ( ( F : B -1-1-onto-> B /\ P e. B ) -> ( F ` ( `' F ` P ) ) = P )
11 5 10 stoic3
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( F ` ( `' F ` P ) ) = P )
12 11 eleq1d
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( F ` ( `' F ` P ) ) e. A <-> P e. A ) )
13 9 12 bitr2d
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( `' F ` P ) e. A ) )