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

Metamath Proof Explorer

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 ⊢ B = Base K
trlnidat.a ⊢ A = Atoms ⁡ K
trlnidat.h ⊢ H = LHyp ⁡ K
trlnidat.t ⊢ T = LTrn ⁡ K ⁡ W
trlnidat.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlnidat ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B → R ⁡ F ∈ A

Proof

Step Hyp Ref Expression
1 trlnidat.b ⊢ B = Base K
2 trlnidat.a ⊢ A = Atoms ⁡ K
3 trlnidat.h ⊢ H = LHyp ⁡ K
4 trlnidat.t ⊢ T = LTrn ⁡ K ⁡ W
5 trlnidat.r ⊢ R = trL ⁡ K ⁡ W
6 eqid ⊢ ≤ K = ≤ K
7 1 6 2 3 4 ltrnnid ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B → ∃ p ∈ A ¬ p ≤ K W ∧ F ⁡ p ≠ p
8 simp11 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → K ∈ HL ∧ W ∈ H
9 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → p ∈ A
10 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → ¬ p ≤ K W
11 simp12 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → F ∈ T
12 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → F ⁡ p ≠ p
13 6 2 3 4 5 trlat ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ∈ T ∧ F ⁡ p ≠ p → R ⁡ F ∈ A
14 8 9 10 11 12 13 syl122anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B ∧ p ∈ A ∧ ¬ p ≤ K W ∧ F ⁡ p ≠ p → R ⁡ F ∈ A
15 14 rexlimdv3a ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B → ∃ p ∈ A ¬ p ≤ K W ∧ F ⁡ p ≠ p → R ⁡ F ∈ A
16 7 15 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ F ≠ I ↾ B → R ⁡ F ∈ A