Metamath Proof Explorer

Theorem lautcvr

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

Ref Expression
Hypotheses lautcvr.b 
|- B = ( Base ` K )
lautcvr.c 
|- C = (
lautcvr.i 
|- I = ( LAut ` K )
Assertion lautcvr 
|- ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 lautcvr.b 
 |-  B = ( Base ` K )
2 lautcvr.c 
 |-  C = (
3 lautcvr.i 
 |-  I = ( LAut ` K )
4 eqid 
 |-  ( lt ` K ) = ( lt ` K )
5 1 4 3 lautlt 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ( lt ` K ) Y <-> ( F ` X ) ( lt ` K ) ( F ` Y ) ) )
6 simpll 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> K e. A )
7 simplr1 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> F e. I )
8 simplr2 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> X e. B )
9 simpr 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> w e. B )
10 1 4 3 lautlt 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ w e. B ) ) -> ( X ( lt ` K ) w <-> ( F ` X ) ( lt ` K ) ( F ` w ) ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( X ( lt ` K ) w <-> ( F ` X ) ( lt ` K ) ( F ` w ) ) )
12 simplr3 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> Y e. B )
13 1 4 3 lautlt 
 |-  ( ( K e. A /\ ( F e. I /\ w e. B /\ Y e. B ) ) -> ( w ( lt ` K ) Y <-> ( F ` w ) ( lt ` K ) ( F ` Y ) ) )
14 6 7 9 12 13 syl13anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( w ( lt ` K ) Y <-> ( F ` w ) ( lt ` K ) ( F ` Y ) ) )
15 11 14 anbi12d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) <-> ( ( F ` X ) ( lt ` K ) ( F ` w ) /\ ( F ` w ) ( lt ` K ) ( F ` Y ) ) ) )
16 1 3 lautcl 
 |-  ( ( ( K e. A /\ F e. I ) /\ w e. B ) -> ( F ` w ) e. B )
17 6 7 9 16 syl21anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( F ` w ) e. B )
18 breq2 
 |-  ( z = ( F ` w ) -> ( ( F ` X ) ( lt ` K ) z <-> ( F ` X ) ( lt ` K ) ( F ` w ) ) )
19 breq1 
 |-  ( z = ( F ` w ) -> ( z ( lt ` K ) ( F ` Y ) <-> ( F ` w ) ( lt ` K ) ( F ` Y ) ) )
20 18 19 anbi12d 
 |-  ( z = ( F ` w ) -> ( ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) <-> ( ( F ` X ) ( lt ` K ) ( F ` w ) /\ ( F ` w ) ( lt ` K ) ( F ` Y ) ) ) )
21 20 rspcev 
 |-  ( ( ( F ` w ) e. B /\ ( ( F ` X ) ( lt ` K ) ( F ` w ) /\ ( F ` w ) ( lt ` K ) ( F ` Y ) ) ) -> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) )
22 21 ex 
 |-  ( ( F ` w ) e. B -> ( ( ( F ` X ) ( lt ` K ) ( F ` w ) /\ ( F ` w ) ( lt ` K ) ( F ` Y ) ) -> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
23 17 22 syl 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( ( ( F ` X ) ( lt ` K ) ( F ` w ) /\ ( F ` w ) ( lt ` K ) ( F ` Y ) ) -> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
24 15 23 sylbid 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ w e. B ) -> ( ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) -> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
25 24 rexlimdva 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) -> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
26 simpll 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> K e. A )
27 simplr1 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> F e. I )
28 simplr2 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> X e. B )
29 1 3 laut1o 
 |-  ( ( K e. A /\ F e. I ) -> F : B -1-1-onto-> B )
30 26 27 29 syl2anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> F : B -1-1-onto-> B )
31 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> B /\ z e. B ) -> ( `' F ` z ) e. B )
32 30 31 sylancom 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( `' F ` z ) e. B )
33 1 4 3 lautlt 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ ( `' F ` z ) e. B ) ) -> ( X ( lt ` K ) ( `' F ` z ) <-> ( F ` X ) ( lt ` K ) ( F ` ( `' F ` z ) ) ) )
34 26 27 28 32 33 syl13anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( X ( lt ` K ) ( `' F ` z ) <-> ( F ` X ) ( lt ` K ) ( F ` ( `' F ` z ) ) ) )
35 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> B /\ z e. B ) -> ( F ` ( `' F ` z ) ) = z )
36 30 35 sylancom 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( F ` ( `' F ` z ) ) = z )
37 36 breq2d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( F ` X ) ( lt ` K ) ( F ` ( `' F ` z ) ) <-> ( F ` X ) ( lt ` K ) z ) )
38 34 37 bitr2d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( F ` X ) ( lt ` K ) z <-> X ( lt ` K ) ( `' F ` z ) ) )
39 simplr3 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> Y e. B )
40 1 4 3 lautlt 
 |-  ( ( K e. A /\ ( F e. I /\ ( `' F ` z ) e. B /\ Y e. B ) ) -> ( ( `' F ` z ) ( lt ` K ) Y <-> ( F ` ( `' F ` z ) ) ( lt ` K ) ( F ` Y ) ) )
41 26 27 32 39 40 syl13anc 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( `' F ` z ) ( lt ` K ) Y <-> ( F ` ( `' F ` z ) ) ( lt ` K ) ( F ` Y ) ) )
42 36 breq1d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( F ` ( `' F ` z ) ) ( lt ` K ) ( F ` Y ) <-> z ( lt ` K ) ( F ` Y ) ) )
43 41 42 bitr2d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( z ( lt ` K ) ( F ` Y ) <-> ( `' F ` z ) ( lt ` K ) Y ) )
44 38 43 anbi12d 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) <-> ( X ( lt ` K ) ( `' F ` z ) /\ ( `' F ` z ) ( lt ` K ) Y ) ) )
45 breq2 
 |-  ( w = ( `' F ` z ) -> ( X ( lt ` K ) w <-> X ( lt ` K ) ( `' F ` z ) ) )
46 breq1 
 |-  ( w = ( `' F ` z ) -> ( w ( lt ` K ) Y <-> ( `' F ` z ) ( lt ` K ) Y ) )
47 45 46 anbi12d 
 |-  ( w = ( `' F ` z ) -> ( ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) <-> ( X ( lt ` K ) ( `' F ` z ) /\ ( `' F ` z ) ( lt ` K ) Y ) ) )
48 47 rspcev 
 |-  ( ( ( `' F ` z ) e. B /\ ( X ( lt ` K ) ( `' F ` z ) /\ ( `' F ` z ) ( lt ` K ) Y ) ) -> E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) )
49 48 ex 
 |-  ( ( `' F ` z ) e. B -> ( ( X ( lt ` K ) ( `' F ` z ) /\ ( `' F ` z ) ( lt ` K ) Y ) -> E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) )
50 32 49 syl 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( X ( lt ` K ) ( `' F ` z ) /\ ( `' F ` z ) ( lt ` K ) Y ) -> E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) )
51 44 50 sylbid 
 |-  ( ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) /\ z e. B ) -> ( ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) -> E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) )
52 51 rexlimdva 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) -> E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) )
53 25 52 impbid 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) <-> E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
54 53 notbid 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( -. E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) <-> -. E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) )
55 5 54 anbi12d 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( X ( lt ` K ) Y /\ -. E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) <-> ( ( F ` X ) ( lt ` K ) ( F ` Y ) /\ -. E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) ) )
56 1 4 2 cvrval 
 |-  ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X ( lt ` K ) Y /\ -. E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) ) )
57 56 3adant3r1 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X C Y <-> ( X ( lt ` K ) Y /\ -. E. w e. B ( X ( lt ` K ) w /\ w ( lt ` K ) Y ) ) ) )
58 simpl 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> K e. A )
59 simpr1 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> F e. I )
60 simpr2 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X e. B )
61 1 3 lautcl 
 |-  ( ( ( K e. A /\ F e. I ) /\ X e. B ) -> ( F ` X ) e. B )
62 58 59 60 61 syl21anc 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) e. B )
63 simpr3 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y e. B )
64 1 3 lautcl 
 |-  ( ( ( K e. A /\ F e. I ) /\ Y e. B ) -> ( F ` Y ) e. B )
65 58 59 63 64 syl21anc 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) e. B )
66 1 4 2 cvrval 
 |-  ( ( K e. A /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( ( F ` X ) C ( F ` Y ) <-> ( ( F ` X ) ( lt ` K ) ( F ` Y ) /\ -. E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) ) )
67 58 62 65 66 syl3anc 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) C ( F ` Y ) <-> ( ( F ` X ) ( lt ` K ) ( F ` Y ) /\ -. E. z e. B ( ( F ` X ) ( lt ` K ) z /\ z ( lt ` K ) ( F ` Y ) ) ) ) )
68 55 57 67 3bitr4d 
 |-  ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )