Theorem ltrn1o

Description: A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrn1o.b	$$⊢B={\mathrm{Base}}_K$$
	ltrn1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrn1o.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrn1o	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F:B\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		ltrn1o.b	$$⊢B={\mathrm{Base}}_K$$
2		ltrn1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		ltrn1o.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		simpll	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to K\in V$$
5		eqid	$$⊢\mathrm{LAut}\left(K\right)=\mathrm{LAut}\left(K\right)$$
6	2 5 3	ltrnlaut	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F\in \mathrm{LAut}\left(K\right)$$
7	1 5	laut1o	$$⊢\left(K\in V\wedge F\in \mathrm{LAut}\left(K\right)\right)\to F:B\underset{1-1\; onto}{⟶}B$$
8	4 6 7	syl2anc	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to F:B\underset{1-1\; onto}{⟶}B$$