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 ‘ 𝐾 )
ltrn2eq.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrn2eq.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrn2eq.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnatneq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝐹𝑄 ) ≠ 𝑄 )

Proof

Step Hyp Ref Expression
1 ltrn2eq.l = ( le ‘ 𝐾 )
2 ltrn2eq.a 𝐴 = ( Atoms ‘ 𝐾 )
3 ltrn2eq.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrn2eq.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 ltrn2ateq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝐹𝑃 ) = 𝑃 ↔ ( 𝐹𝑄 ) = 𝑄 ) )
6 5 necon3bid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝐹𝑃 ) ≠ 𝑃 ↔ ( 𝐹𝑄 ) ≠ 𝑄 ) )
7 6 biimp3a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝐹𝑄 ) ≠ 𝑄 )