Metamath Proof Explorer


Theorem ltrnnid

Description: If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom W and not equal to its translation. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses ltrneq.b 𝐵 = ( Base ‘ 𝐾 )
ltrneq.l = ( le ‘ 𝐾 )
ltrneq.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrneq.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrneq.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnnid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) )

Proof

Step Hyp Ref Expression
1 ltrneq.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrneq.l = ( le ‘ 𝐾 )
3 ltrneq.a 𝐴 = ( Atoms ‘ 𝐾 )
4 ltrneq.h 𝐻 = ( LHyp ‘ 𝐾 )
5 ltrneq.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 ralinexa ( ∀ 𝑝𝐴 ( ¬ 𝑝 𝑊 → ¬ ( 𝐹𝑝 ) ≠ 𝑝 ) ↔ ¬ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) )
7 nne ( ¬ ( 𝐹𝑝 ) ≠ 𝑝 ↔ ( 𝐹𝑝 ) = 𝑝 )
8 7 biimpi ( ¬ ( 𝐹𝑝 ) ≠ 𝑝 → ( 𝐹𝑝 ) = 𝑝 )
9 8 imim2i ( ( ¬ 𝑝 𝑊 → ¬ ( 𝐹𝑝 ) ≠ 𝑝 ) → ( ¬ 𝑝 𝑊 → ( 𝐹𝑝 ) = 𝑝 ) )
10 9 ralimi ( ∀ 𝑝𝐴 ( ¬ 𝑝 𝑊 → ¬ ( 𝐹𝑝 ) ≠ 𝑝 ) → ∀ 𝑝𝐴 ( ¬ 𝑝 𝑊 → ( 𝐹𝑝 ) = 𝑝 ) )
11 6 10 sylbir ( ¬ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) → ∀ 𝑝𝐴 ( ¬ 𝑝 𝑊 → ( 𝐹𝑝 ) = 𝑝 ) )
12 1 2 3 4 5 ltrnid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ∀ 𝑝𝐴 ( ¬ 𝑝 𝑊 → ( 𝐹𝑝 ) = 𝑝 ) ↔ 𝐹 = ( I ↾ 𝐵 ) ) )
13 11 12 syl5ib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ¬ ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) → 𝐹 = ( I ↾ 𝐵 ) ) )
14 13 necon1ad ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) ) )
15 14 3impia ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑝𝐴 ( ¬ 𝑝 𝑊 ∧ ( 𝐹𝑝 ) ≠ 𝑝 ) )