Metamath Proof Explorer


Theorem ltrnatneq

Description: If any atom (under W ) is not equal to its translation, so is any other atom. TODO: -. P .<_ W isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (Contributed by NM, 6-May-2013)

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

Proof

Step Hyp Ref Expression
1 ltrn2eq.l
 |-  .<_ = ( le ` K )
2 ltrn2eq.a
 |-  A = ( Atoms ` K )
3 ltrn2eq.h
 |-  H = ( LHyp ` K )
4 ltrn2eq.t
 |-  T = ( ( LTrn ` K ) ` W )
5 1 2 3 4 ltrn2ateq
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( F ` P ) = P <-> ( F ` Q ) = Q ) )
6 5 necon3bid
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( F ` P ) =/= P <-> ( F ` Q ) =/= Q ) )
7 6 biimp3a
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F ` P ) =/= P ) -> ( F ` Q ) =/= Q )