Metamath Proof Explorer

Theorem trlator0

Description: The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013)

Ref Expression
Hypotheses trl0a.z 
|- .0. = ( 0. ` K )
trl0a.a 
|- A = ( Atoms ` K )
trl0a.h 
|- H = ( LHyp ` K )
trl0a.t 
|- T = ( ( LTrn ` K ) ` W )
trl0a.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlator0 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A \/ ( R ` F ) = .0. ) )

Proof

Step Hyp Ref Expression
1 trl0a.z 
 |-  .0. = ( 0. ` K )
2 trl0a.a 
 |-  A = ( Atoms ` K )
3 trl0a.h 
 |-  H = ( LHyp ` K )
4 trl0a.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 trl0a.r 
 |-  R = ( ( trL ` K ) ` W )
6 df-ne 
 |-  ( ( R ` F ) =/= .0. <-> -. ( R ` F ) = .0. )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 7 2 3 lhpexnle 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A -. p ( le ` K ) W )
9 8 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) -> E. p e. A -. p ( le ` K ) W )
10 simplll 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
11 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( p e. A /\ -. p ( le ` K ) W ) )
12 simpllr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> F e. T )
13 simplr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( R ` F ) =/= .0. )
14 10 adantr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) /\ ( F ` p ) = p ) -> ( K e. HL /\ W e. H ) )
15 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) /\ ( F ` p ) = p ) -> ( p e. A /\ -. p ( le ` K ) W ) )
16 12 adantr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) /\ ( F ` p ) = p ) -> F e. T )
17 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) /\ ( F ` p ) = p ) -> ( F ` p ) = p )
18 7 1 2 3 4 5 trl0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ -. p ( le ` K ) W ) /\ ( F e. T /\ ( F ` p ) = p ) ) -> ( R ` F ) = .0. )
19 14 15 16 17 18 syl112anc 
 |-  ( ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) /\ ( F ` p ) = p ) -> ( R ` F ) = .0. )
20 19 ex 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( ( F ` p ) = p -> ( R ` F ) = .0. ) )
21 20 necon3d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( ( R ` F ) =/= .0. -> ( F ` p ) =/= p ) )
22 13 21 mpd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( F ` p ) =/= p )
23 7 2 3 4 5 trlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ -. p ( le ` K ) W ) /\ ( F e. T /\ ( F ` p ) =/= p ) ) -> ( R ` F ) e. A )
24 10 11 12 22 23 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) /\ ( p e. A /\ -. p ( le ` K ) W ) ) -> ( R ` F ) e. A )
25 9 24 rexlimddv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) =/= .0. ) -> ( R ` F ) e. A )
26 25 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) =/= .0. -> ( R ` F ) e. A ) )
27 6 26 syl5bir 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( -. ( R ` F ) = .0. -> ( R ` F ) e. A ) )
28 27 orrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) = .0. \/ ( R ` F ) e. A ) )
29 28 orcomd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A \/ ( R ` F ) = .0. ) )