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

Metamath Proof Explorer

Theorem ltrn11at

Description: Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013)

Ref Expression
Hypotheses ltrneq2.a ⊢ A = Atoms ⁡ K
ltrneq2.h ⊢ H = LHyp ⁡ K
ltrneq2.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrn11at ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → F ⁡ P ≠ F ⁡ Q

Proof

Step Hyp Ref Expression
1 ltrneq2.a ⊢ A = Atoms ⁡ K
2 ltrneq2.h ⊢ H = LHyp ⁡ K
3 ltrneq2.t ⊢ T = LTrn ⁡ K ⁡ W
4 simp33 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ≠ Q
5 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → K ∈ HL ∧ W ∈ H
6 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → F ∈ T
7 simp31 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ∈ A
8 eqid ⊢ Base K = Base K
9 8 1 atbase ⊢ P ∈ A → P ∈ Base K
10 7 9 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ∈ Base K
11 simp32 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → Q ∈ A
12 8 1 atbase ⊢ Q ∈ A → Q ∈ Base K
13 11 12 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → Q ∈ Base K
14 8 2 3 ltrn11 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ Base K ∧ Q ∈ Base K → F ⁡ P = F ⁡ Q ↔ P = Q
15 5 6 10 13 14 syl112anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → F ⁡ P = F ⁡ Q ↔ P = Q
16 15 necon3bid ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → F ⁡ P ≠ F ⁡ Q ↔ P ≠ Q
17 4 16 mpbird ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → F ⁡ P ≠ F ⁡ Q