This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ¬ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → 𝐹 = ( I ↾ 𝐵 ) ) )
14 13 necon1ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) )
15 14 3impia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) )