Metamath Proof Explorer


Theorem lautlt

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

Ref Expression
Hypotheses lautlt.b 𝐵 = ( Base ‘ 𝐾 )
lautlt.s < = ( lt ‘ 𝐾 )
lautlt.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝐹𝑋 ) < ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautlt.b 𝐵 = ( Base ‘ 𝐾 )
2 lautlt.s < = ( lt ‘ 𝐾 )
3 lautlt.i 𝐼 = ( LAut ‘ 𝐾 )
4 simpl ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐾𝐴 )
5 simpr1 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐹𝐼 )
6 simpr2 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
7 simpr3 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
8 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 1 8 3 lautle ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑋 ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
10 4 5 6 7 9 syl22anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑋 ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
11 1 3 laut11 ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ↔ 𝑋 = 𝑌 ) )
12 4 5 6 7 11 syl22anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ↔ 𝑋 = 𝑌 ) )
13 12 bicomd ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 = 𝑌 ↔ ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ) )
14 13 necon3bid ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋𝑌 ↔ ( 𝐹𝑋 ) ≠ ( 𝐹𝑌 ) ) )
15 10 14 anbi12d ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌𝑋𝑌 ) ↔ ( ( 𝐹𝑋 ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ( 𝐹𝑋 ) ≠ ( 𝐹𝑌 ) ) ) )
16 8 2 pltval ( ( 𝐾𝐴𝑋𝐵𝑌𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌𝑋𝑌 ) ) )
17 16 3adant3r1 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌𝑋𝑌 ) ) )
18 1 3 lautcl ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ 𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ 𝐵 )
19 4 5 6 18 syl21anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑋 ) ∈ 𝐵 )
20 1 3 lautcl ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ 𝑌𝐵 ) → ( 𝐹𝑌 ) ∈ 𝐵 )
21 4 5 7 20 syl21anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑌 ) ∈ 𝐵 )
22 8 2 pltval ( ( 𝐾𝐴 ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) → ( ( 𝐹𝑋 ) < ( 𝐹𝑌 ) ↔ ( ( 𝐹𝑋 ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ( 𝐹𝑋 ) ≠ ( 𝐹𝑌 ) ) ) )
23 4 19 21 22 syl3anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) < ( 𝐹𝑌 ) ↔ ( ( 𝐹𝑋 ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ( 𝐹𝑋 ) ≠ ( 𝐹𝑌 ) ) ) )
24 15 17 23 3bitr4d ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝐹𝑋 ) < ( 𝐹𝑌 ) ) )