ltrn11

Description: One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrn1o.b	$⊢ B = {Base}_{K}$
	ltrn1o.h	$⊢ H = LHyp (K)$
	ltrn1o.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrn11	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (F (X) = F (Y) \leftrightarrow X = Y)$

Step	Hyp	Ref	Expression
1		ltrn1o.b	$⊢ B = {Base}_{K}$
2		ltrn1o.h	$⊢ H = LHyp (K)$
3		ltrn1o.t	$⊢ T = LTrn (K) (W)$
4		simp1l	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to K \in V$
5		eqid	$⊢ LAut (K) = LAut (K)$
6	2 5 3	ltrnlaut	$⊢ ((K \in V \land W \in H) \land F \in T) \to F \in LAut (K)$
7	6	3adant3	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to F \in LAut (K)$
8		simp3l	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to X \in B$
9		simp3r	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to Y \in B$
10	1 5	laut11	$⊢ ((K \in V \land F \in LAut (K)) \land (X \in B \land Y \in B)) \to (F (X) = F (Y) \leftrightarrow X = Y)$
11	4 7 8 9 10	syl22anc	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land Y \in B)) \to (F (X) = F (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer