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

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 ⊢ ≤ ˙ = ≤ K
trlne.a ⊢ A = Atoms ⁡ K
trlne.h ⊢ H = LHyp ⁡ K
trlne.t ⊢ T = LTrn ⁡ K ⁡ W
trlne.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlne ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≠ R ⁡ F

Proof

Step Hyp Ref Expression
1 trlne.l ⊢ ≤ ˙ = ≤ K
2 trlne.a ⊢ A = Atoms ⁡ K
3 trlne.h ⊢ H = LHyp ⁡ K
4 trlne.t ⊢ T = LTrn ⁡ K ⁡ W
5 trlne.r ⊢ R = trL ⁡ K ⁡ W
6 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ¬ P ≤ ˙ W
7 1 3 4 5 trlle ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ≤ ˙ W
8 7 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F ≤ ˙ W
9 breq1 ⊢ P = R ⁡ F → P ≤ ˙ W ↔ R ⁡ F ≤ ˙ W
10 8 9 syl5ibrcom ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P = R ⁡ F → P ≤ ˙ W
11 10 necon3bd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ¬ P ≤ ˙ W → P ≠ R ⁡ F
12 6 11 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≠ R ⁡ F