Metamath Proof Explorer

Theorem ltrnatb

Description: The lattice translation of an atom is an atom. (Contributed by NM, 20-May-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 ltrnatb 
|- ( ( ( 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 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> P e. B )
6 1 3 4 ltrncl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( F ` P ) e. B )
7 5 6 2thd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. B <-> ( F ` P ) e. B ) )
8 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( K e. HL /\ W e. H ) )
9 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> F e. T )
10 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> K e. HL )
11 hlop 
 |-  ( K e. HL -> K e. OP )
12 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
13 1 12 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. B )
14 10 11 13 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( 0. ` K ) e. B )
15 eqid 
 |-  (
16 1 15 3 4 ltrncvr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( 0. ` K ) e. B /\ P e. B ) ) -> ( ( 0. ` K ) (  ( F ` ( 0. ` K ) ) (
17 8 9 14 5 16 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( 0. ` K ) (  ( F ` ( 0. ` K ) ) (
18 10 11 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> K e. OP )
19 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> W e. H )
20 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
21 19 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> W e. B )
22 eqid 
 |-  ( le ` K ) = ( le ` K )
23 1 22 12 op0le 
 |-  ( ( K e. OP /\ W e. B ) -> ( 0. ` K ) ( le ` K ) W )
24 18 21 23 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( 0. ` K ) ( le ` K ) W )
25 1 22 3 4 ltrnval1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( ( 0. ` K ) e. B /\ ( 0. ` K ) ( le ` K ) W ) ) -> ( F ` ( 0. ` K ) ) = ( 0. ` K ) )
26 8 9 14 24 25 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( F ` ( 0. ` K ) ) = ( 0. ` K ) )
27 26 breq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( F ` ( 0. ` K ) ) (  ( 0. ` K ) (
28 17 27 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( 0. ` K ) (  ( 0. ` K ) (
29 7 28 anbi12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( P e. B /\ ( 0. ` K ) (  ( ( F ` P ) e. B /\ ( 0. ` K ) (
30 1 12 15 2 isat 
 |-  ( K e. HL -> ( P e. A <-> ( P e. B /\ ( 0. ` K ) (
31 10 30 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( P e. B /\ ( 0. ` K ) (
32 1 12 15 2 isat 
 |-  ( K e. HL -> ( ( F ` P ) e. A <-> ( ( F ` P ) e. B /\ ( 0. ` K ) (
33 10 32 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( F ` P ) e. A <-> ( ( F ` P ) e. B /\ ( 0. ` K ) (
34 29 31 33 3bitr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( F ` P ) e. A ) )