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 \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to F (P) \neq 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 \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to P \neq Q$
5		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to (K \in HL \land W \in H)$
6		simp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to F \in T$
7		simp31	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to P \in A$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 1	atbase	$⊢ P \in A \to P \in {Base}_{K}$
10	7 9	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to P \in {Base}_{K}$
11		simp32	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to Q \in A$
12	8 1	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to Q \in {Base}_{K}$
14	8 2 3	ltrn11	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in {Base}_{K} \land Q \in {Base}_{K})) \to (F (P) = F (Q) \leftrightarrow P = Q)$
15	5 6 10 13 14	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to (F (P) = F (Q) \leftrightarrow P = Q)$
16	15	necon3bid	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to (F (P) \neq F (Q) \leftrightarrow P \neq Q)$
17	4 16	mpbird	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to F (P) \neq F (Q)$