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 
|- .< = ( lt ` K )
lautlt.i 
|- I = ( LAut ` K )
Assertion lautlt 
|- ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X .< Y <-> ( F ` X ) .< ( F ` Y ) ) )

Proof

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