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