Theorem trlne

Description: The trace of a lattice translation is not equal to any atom not under the fiducial co-atom W . Part of proof of Lemma C in Crawley p. 112. (Contributed by NM, 25-May-2012)

	Ref	Expression
Hypotheses	trlne.l	⊢ ≤ = ( le ‘ 𝐾 )
	trlne.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	trlne.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlne.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trlne.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlne	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≠ ( 𝑅 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		trlne.l	⊢ ≤ = ( le ‘ 𝐾 )
2		trlne.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		trlne.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trlne.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		trlne.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ¬ 𝑃 ≤ 𝑊 )
7	1 3 4 5	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
8	7	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
9		breq1	⊢ ( 𝑃 = ( 𝑅 ‘ 𝐹 ) → ( 𝑃 ≤ 𝑊 ↔ ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ) )
10	8 9	syl5ibrcom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 = ( 𝑅 ‘ 𝐹 ) → 𝑃 ≤ 𝑊 ) )
11	10	necon3bd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ¬ 𝑃 ≤ 𝑊 → 𝑃 ≠ ( 𝑅 ‘ 𝐹 ) ) )
12	6 11	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → 𝑃 ≠ ( 𝑅 ‘ 𝐹 ) )