Theorem ltrnnid

Description: If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom W and not equal to its translation. (Contributed by NM, 24-May-2012)

	Ref	Expression
Hypotheses	ltrneq.b	|- B = ( Base ` K )
	ltrneq.l	|- .<_ = ( le ` K )
	ltrneq.a	|- A = ( Atoms ` K )
	ltrneq.h	|- H = ( LHyp ` K )
	ltrneq.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrnnid	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) )

Proof

Step	Hyp	Ref	Expression
1		ltrneq.b	|- B = ( Base ` K )
2		ltrneq.l	|- .<_ = ( le ` K )
3		ltrneq.a	|- A = ( Atoms ` K )
4		ltrneq.h	|- H = ( LHyp ` K )
5		ltrneq.t	|- T = ( ( LTrn ` K ) ` W )
6		ralinexa	|- ( A. p e. A ( -. p .<_ W -> -. ( F ` p ) =/= p ) <-> -. E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) )
7		nne	|- ( -. ( F ` p ) =/= p <-> ( F ` p ) = p )
8	7	biimpi	|- ( -. ( F ` p ) =/= p -> ( F ` p ) = p )
9	8	imim2i	|- ( ( -. p .<_ W -> -. ( F ` p ) =/= p ) -> ( -. p .<_ W -> ( F ` p ) = p ) )
10	9	ralimi	|- ( A. p e. A ( -. p .<_ W -> -. ( F ` p ) =/= p ) -> A. p e. A ( -. p .<_ W -> ( F ` p ) = p ) )
11	6 10	sylbir	|- ( -. E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) -> A. p e. A ( -. p .<_ W -> ( F ` p ) = p ) )
12	1 2 3 4 5	ltrnid	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( A. p e. A ( -. p .<_ W -> ( F ` p ) = p ) <-> F = ( _I |` B ) ) )
13	11 12	syl5ib	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( -. E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) -> F = ( _I |` B ) ) )
14	13	necon1ad	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F =/= ( _I |` B ) -> E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) ) )
15	14	3impia	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) )