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 ) )