Theorem trlnidat

Description: The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in Crawley p. 112. (Contributed by NM, 23-May-2012)

	Ref	Expression
Hypotheses	trlnidat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	trlnidat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	trlnidat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlnidat.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trlnidat.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlnidat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		trlnidat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		trlnidat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		trlnidat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trlnidat.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		trlnidat.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7	1 6 2 3 4	ltrnnid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) )
8		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → 𝑝 ∈ 𝐴 )
10		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
11		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → 𝐹 ∈ 𝑇 )
12		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 )
13	6 2 3 4 5	trlat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
14	8 9 10 11 12 13	syl122anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
15	14	rexlimdv3a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
16	7 15	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )