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 ↾ 𝐵 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) )