Theorem laut11

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

	Ref	Expression
Hypotheses	laut1o.b	$$⊢B={\mathrm{Base}}_K$$
	laut1o.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
Assertion	laut11	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(F\left(X\right)=F\left(Y\right)\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		laut1o.b	$$⊢B={\mathrm{Base}}_K$$
2		laut1o.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
3	1 2	laut1o	$$⊢\left(K\in V\wedge F\in I\right)\to F:B\underset{1-1\; onto}{⟶}B$$
4		f1of1	$$⊢F:B\underset{1-1\; onto}{⟶}B\to F:B\underset{1-1}{⟶}B$$
5	3 4	syl	$$⊢\left(K\in V\wedge F\in I\right)\to F:B\underset{1-1}{⟶}B$$
6		f1fveq	$$⊢\left(F:B\underset{1-1}{⟶}B\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(F\left(X\right)=F\left(Y\right)\leftrightarrow X=Y\right)$$
7	5 6	sylan	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(F\left(X\right)=F\left(Y\right)\leftrightarrow X=Y\right)$$