Theorem trlne

Description: The trace of a lattice translation is not equal to any atom not under the fiducial co-atom W . Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)

	Ref	Expression
Hypotheses	trlne.l	|- .<_ = ( le ` K )
	trlne.a	|- A = ( Atoms ` K )
	trlne.h	|- H = ( LHyp ` K )
	trlne.t	|- T = ( ( LTrn ` K ) ` W )
	trlne.r	|- R = ( ( trL ` K ) ` W )
Assertion	trlne	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P =/= ( R ` F ) )

Proof

Step	Hyp	Ref	Expression
1		trlne.l	|- .<_ = ( le ` K )
2		trlne.a	|- A = ( Atoms ` K )
3		trlne.h	|- H = ( LHyp ` K )
4		trlne.t	|- T = ( ( LTrn ` K ) ` W )
5		trlne.r	|- R = ( ( trL ` K ) ` W )
6		simp3r	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. P .<_ W )
7	1 3 4 5	trlle	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )
8	7	3adant3	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) .<_ W )
9		breq1	|- ( P = ( R ` F ) -> ( P .<_ W <-> ( R ` F ) .<_ W ) )
10	8 9	syl5ibrcom	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P = ( R ` F ) -> P .<_ W ) )
11	10	necon3bd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( -. P .<_ W -> P =/= ( R ` F ) ) )
12	6 11	mpd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P =/= ( R ` F ) )