This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trlatn0

Description: The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-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 trlatn0 
|- ( ( ( 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 hlatl 
 |-  ( K e. HL -> K e. AtLat )
7 6 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) e. A ) -> K e. AtLat )
8 1 2 atn0 
 |-  ( ( K e. AtLat /\ ( R ` F ) e. A ) -> ( R ` F ) =/= .0. )
9 7 8 sylancom 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( R ` F ) e. A ) -> ( R ` F ) =/= .0. )
10 9 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A -> ( R ` F ) =/= .0. ) )
11 1 2 3 4 5 trlator0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A \/ ( R ` F ) = .0. ) )
12 11 ord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( -. ( R ` F ) e. A -> ( R ` F ) = .0. ) )
13 12 necon1ad 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) =/= .0. -> ( R ` F ) e. A ) )
14 10 13 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A <-> ( R ` F ) =/= .0. ) )