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