Metamath Proof Explorer


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 ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃 ≠ ( 𝑅𝐹 ) )