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