Theorem lautle

Description: Less-than or equal property of a lattice automorphism. (Contributed by NM, 19-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lautset.b	$$⊢B={\mathrm{Base}}_K$$
2		lautset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lautset.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
4	1 2 3	islaut	$$⊢K\in V\to \left(F\in I\leftrightarrow \left(F:B\underset{1-1\; onto}{⟶}B\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\right)\right)\right)$$
5	4	simplbda	$$⊢\left(K\in V\wedge F\in I\right)\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\right)$$
6		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
7		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
8	7	breq1d	$$⊢x=X\to \left(F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(y\right)\right)$$
9	6 8	bibi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }y\leftrightarrow F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }y\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(y\right)\right)\right)$$
10		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
11		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
12	11	breq2d	$$⊢y=Y\to \left(F\left(X\right)\underset{\dot{}}{\le }F\left(y\right)\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(Y\right)\right)$$
13	10 12	bibi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }y\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(y\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(Y\right)\right)\right)$$
14	9 13	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\leftrightarrow F\left(x\right)\underset{\dot{}}{\le }F\left(y\right)\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(Y\right)\right)\right)$$
15	5 14	mpan9	$$⊢\left(\left(K\in V\wedge F\in I\right)\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow F\left(X\right)\underset{\dot{}}{\le }F\left(Y\right)\right)$$