ltrn1o

Description: A lattice translation is a one-to-one onto function. (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	ltrn1o	$⊢ ((K \in V \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$

Step	Hyp	Ref	Expression
1		ltrn1o.b	$⊢ B = {Base}_{K}$
2		ltrn1o.h	$⊢ H = LHyp (K)$
3		ltrn1o.t	$⊢ T = LTrn (K) (W)$
4		simpll	$⊢ ((K \in V \land W \in H) \land F \in T) \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	1 5	laut1o	$⊢ (K \in V \land F \in LAut (K)) \to F : B \underset{1-1 onto}{⟶} B$
8	4 6 7	syl2anc	$⊢ ((K \in V \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer