Metamath Proof Explorer


Theorem lautcvr

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

Ref Expression
Hypotheses lautcvr.b 𝐵 = ( Base ‘ 𝐾 )
lautcvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
lautcvr.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautcvr ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautcvr.b 𝐵 = ( Base ‘ 𝐾 )
2 lautcvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 lautcvr.i 𝐼 = ( LAut ‘ 𝐾 )
4 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
5 1 4 3 lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
6 simpll ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → 𝐾𝐴 )
7 simplr1 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → 𝐹𝐼 )
8 simplr2 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → 𝑋𝐵 )
9 simpr ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → 𝑤𝐵 )
10 1 4 3 lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑤𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ) )
11 6 7 8 9 10 syl13anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤 ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ) )
12 simplr3 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → 𝑌𝐵 )
13 1 4 3 lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑤𝐵𝑌𝐵 ) ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
14 6 7 9 12 13 syl13anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
15 11 14 anbi12d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ∧ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
16 1 3 lautcl ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ 𝑤𝐵 ) → ( 𝐹𝑤 ) ∈ 𝐵 )
17 6 7 9 16 syl21anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( 𝐹𝑤 ) ∈ 𝐵 )
18 breq2 ( 𝑧 = ( 𝐹𝑤 ) → ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ) )
19 breq1 ( 𝑧 = ( 𝐹𝑤 ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ↔ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
20 18 19 anbi12d ( 𝑧 = ( 𝐹𝑤 ) → ( ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ↔ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ∧ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
21 20 rspcev ( ( ( 𝐹𝑤 ) ∈ 𝐵 ∧ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ∧ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) → ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
22 21 ex ( ( 𝐹𝑤 ) ∈ 𝐵 → ( ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ∧ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) → ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
23 17 22 syl ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑤 ) ∧ ( 𝐹𝑤 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) → ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
24 15 23 sylbid ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑤𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
25 24 rexlimdva ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
26 simpll ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → 𝐾𝐴 )
27 simplr1 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → 𝐹𝐼 )
28 simplr2 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → 𝑋𝐵 )
29 1 3 laut1o ( ( 𝐾𝐴𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )
30 26 27 29 syl2anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → 𝐹 : 𝐵1-1-onto𝐵 )
31 f1ocnvdm ( ( 𝐹 : 𝐵1-1-onto𝐵𝑧𝐵 ) → ( 𝐹𝑧 ) ∈ 𝐵 )
32 30 31 sylancom ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( 𝐹𝑧 ) ∈ 𝐵 )
33 1 4 3 lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵 ∧ ( 𝐹𝑧 ) ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑧 ) ) ) )
34 26 27 28 32 33 syl13anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑧 ) ) ) )
35 f1ocnvfv2 ( ( 𝐹 : 𝐵1-1-onto𝐵𝑧𝐵 ) → ( 𝐹 ‘ ( 𝐹𝑧 ) ) = 𝑧 )
36 30 35 sylancom ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( 𝐹 ‘ ( 𝐹𝑧 ) ) = 𝑧 )
37 36 breq2d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑧 ) ) ↔ ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧 ) )
38 34 37 bitr2d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ) )
39 simplr3 ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → 𝑌𝐵 )
40 1 4 3 lautlt ( ( 𝐾𝐴 ∧ ( 𝐹𝐼 ∧ ( 𝐹𝑧 ) ∈ 𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝐹𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
41 26 27 32 39 40 syl13anc ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝐹𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
42 36 breq1d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( 𝐹 ‘ ( 𝐹𝑧 ) ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ↔ 𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
43 41 42 bitr2d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ↔ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) )
44 38 43 anbi12d ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) )
45 breq2 ( 𝑤 = ( 𝐹𝑧 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ) )
46 breq1 ( 𝑤 = ( 𝐹𝑧 ) → ( 𝑤 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) )
47 45 46 anbi12d ( 𝑤 = ( 𝐹𝑧 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) )
48 47 rspcev ( ( ( 𝐹𝑧 ) ∈ 𝐵 ∧ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) )
49 48 ex ( ( 𝐹𝑧 ) ∈ 𝐵 → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
50 32 49 syl ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
51 44 50 sylbid ( ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) ∧ 𝑧𝐵 ) → ( ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) → ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
52 51 rexlimdva ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) → ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) )
53 25 52 impbid ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
54 53 notbid ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ¬ ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ¬ ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) )
55 5 54 anbi12d ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ↔ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ¬ ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) ) )
56 1 4 2 cvrval ( ( 𝐾𝐴𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ) )
57 56 3adant3r1 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑤𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑤𝑤 ( lt ‘ 𝐾 ) 𝑌 ) ) ) )
58 simpl ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐾𝐴 )
59 simpr1 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐹𝐼 )
60 simpr2 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
61 1 3 lautcl ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ 𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ 𝐵 )
62 58 59 60 61 syl21anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑋 ) ∈ 𝐵 )
63 simpr3 ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
64 1 3 lautcl ( ( ( 𝐾𝐴𝐹𝐼 ) ∧ 𝑌𝐵 ) → ( 𝐹𝑌 ) ∈ 𝐵 )
65 58 59 63 64 syl21anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑌 ) ∈ 𝐵 )
66 1 4 2 cvrval ( ( 𝐾𝐴 ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) → ( ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ↔ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ¬ ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) ) )
67 58 62 65 66 syl3anc ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ↔ ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ∧ ¬ ∃ 𝑧𝐵 ( ( 𝐹𝑋 ) ( lt ‘ 𝐾 ) 𝑧𝑧 ( lt ‘ 𝐾 ) ( 𝐹𝑌 ) ) ) ) )
68 55 57 67 3bitr4d ( ( 𝐾𝐴 ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ) )