Theorem trlid0b

Description: A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trlid0b.b	|- B = ( Base ` K )
	trlid0b.z	|- .0. = ( 0. ` K )
	trlid0b.h	|- H = ( LHyp ` K )
	trlid0b.t	|- T = ( ( LTrn ` K ) ` W )
	trlid0b.r	|- R = ( ( trL ` K ) ` W )
Assertion	trlid0b	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F = ( _I |` B ) <-> ( R ` F ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		trlid0b.b	|- B = ( Base ` K )
2		trlid0b.z	|- .0. = ( 0. ` K )
3		trlid0b.h	|- H = ( LHyp ` K )
4		trlid0b.t	|- T = ( ( LTrn ` K ) ` W )
5		trlid0b.r	|- R = ( ( trL ` K ) ` W )
6		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
7	1 6 3 4 5	trlnidatb	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F =/= ( _I |` B ) <-> ( R ` F ) e. ( Atoms ` K ) ) )
8	2 6 3 4 5	trlatn0	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. ( Atoms ` K ) <-> ( R ` F ) =/= .0. ) )
9	7 8	bitrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F =/= ( _I |` B ) <-> ( R ` F ) =/= .0. ) )
10	9	necon4bid	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F = ( _I |` B ) <-> ( R ` F ) = .0. ) )