Metamath Proof Explorer


Theorem lautlt

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

Ref Expression
Hypotheses lautlt.b B = Base K
lautlt.s < ˙ = < K
lautlt.i I = LAut K
Assertion lautlt K A F I X B Y B X < ˙ Y F X < ˙ F Y

Proof

Step Hyp Ref Expression
1 lautlt.b B = Base K
2 lautlt.s < ˙ = < K
3 lautlt.i I = LAut K
4 simpl K A F I X B Y B K A
5 simpr1 K A F I X B Y B F I
6 simpr2 K A F I X B Y B X B
7 simpr3 K A F I X B Y B Y B
8 eqid K = K
9 1 8 3 lautle K A F I X B Y B X K Y F X K F Y
10 4 5 6 7 9 syl22anc K A F I X B Y B X K Y F X K F Y
11 1 3 laut11 K A F I X B Y B F X = F Y X = Y
12 4 5 6 7 11 syl22anc K A F I X B Y B F X = F Y X = Y
13 12 bicomd K A F I X B Y B X = Y F X = F Y
14 13 necon3bid K A F I X B Y B X Y F X F Y
15 10 14 anbi12d K A F I X B Y B X K Y X Y F X K F Y F X F Y
16 8 2 pltval K A X B Y B X < ˙ Y X K Y X Y
17 16 3adant3r1 K A F I X B Y B X < ˙ Y X K Y X Y
18 1 3 lautcl K A F I X B F X B
19 4 5 6 18 syl21anc K A F I X B Y B F X B
20 1 3 lautcl K A F I Y B F Y B
21 4 5 7 20 syl21anc K A F I X B Y B F Y B
22 8 2 pltval K A F X B F Y B F X < ˙ F Y F X K F Y F X F Y
23 4 19 21 22 syl3anc K A F I X B Y B F X < ˙ F Y F X K F Y F X F Y
24 15 17 23 3bitr4d K A F I X B Y B X < ˙ Y F X < ˙ F Y