Metamath Proof Explorer


Theorem lautm

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

Ref Expression
Hypotheses lautm.b 𝐵 = ( Base ‘ 𝐾 )
lautm.m = ( meet ‘ 𝐾 )
lautm.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautm ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautm.b 𝐵 = ( Base ‘ 𝐾 )
2 lautm.m = ( meet ‘ 𝐾 )
3 lautm.i 𝐼 = ( LAut ‘ 𝐾 )
4 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 simpl ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐾 ∈ Lat )
6 simpr1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐹𝐼 )
7 5 6 jca ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) )
8 1 2 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
9 8 3adant3r1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
10 1 3 lautcl ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( 𝑋 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ∈ 𝐵 )
11 7 9 10 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ∈ 𝐵 )
12 simpr2 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
13 1 3 lautcl ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ 𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ 𝐵 )
14 7 12 13 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑋 ) ∈ 𝐵 )
15 simpr3 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
16 1 3 lautcl ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ 𝑌𝐵 ) → ( 𝐹𝑌 ) ∈ 𝐵 )
17 7 15 16 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹𝑌 ) ∈ 𝐵 )
18 1 2 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 )
19 5 14 17 18 syl3anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 )
20 1 4 2 latmle1 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
21 20 3adant3r1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
22 1 4 3 lautle ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( ( 𝑋 𝑌 ) ∈ 𝐵𝑋𝐵 ) ) → ( ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ) )
23 7 9 12 22 syl12anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ) )
24 21 23 mpbid ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) )
25 1 4 2 latmle2 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
26 25 3adant3r1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
27 1 4 3 lautle ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( ( 𝑋 𝑌 ) ∈ 𝐵𝑌𝐵 ) ) → ( ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
28 7 9 15 27 syl12anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑋 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) )
29 26 28 mpbid ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) )
30 1 4 2 latlem12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ∧ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) )
31 5 11 14 17 30 syl13anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ∧ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ) ↔ ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) )
32 24 29 31 mpbi2and ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
33 1 3 laut1o ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )
34 33 3ad2antr1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → 𝐹 : 𝐵1-1-onto𝐵 )
35 f1ocnvfv2 ( ( 𝐹 : 𝐵1-1-onto𝐵 ∧ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
36 34 19 35 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
37 1 4 2 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) )
38 5 14 17 37 syl3anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) )
39 1 4 3 lautcnvle ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹𝑋 ) ∈ 𝐵 ) ) → ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑋 ) ) ) )
40 7 19 14 39 syl12anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑋 ) ) ) )
41 38 40 mpbid ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑋 ) ) )
42 f1ocnvfv1 ( ( 𝐹 : 𝐵1-1-onto𝐵𝑋𝐵 ) → ( 𝐹 ‘ ( 𝐹𝑋 ) ) = 𝑋 )
43 34 12 42 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝐹𝑋 ) ) = 𝑋 )
44 41 43 breqtrd ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 )
45 1 4 2 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝑋 ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) )
46 5 14 17 45 syl3anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) )
47 1 4 3 lautcnvle ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 ∧ ( 𝐹𝑌 ) ∈ 𝐵 ) ) → ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑌 ) ) ) )
48 7 19 17 47 syl12anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹𝑌 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑌 ) ) ) )
49 46 48 mpbid ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝐹𝑌 ) ) )
50 f1ocnvfv1 ( ( 𝐹 : 𝐵1-1-onto𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( 𝐹𝑌 ) ) = 𝑌 )
51 34 15 50 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝐹𝑌 ) ) = 𝑌 )
52 49 51 breqtrd ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 )
53 f1ocnvdm ( ( 𝐹 : 𝐵1-1-onto𝐵 ∧ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ∈ 𝐵 )
54 34 19 53 syl2anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ∈ 𝐵 )
55 1 4 2 latlem12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ∈ 𝐵𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 𝑌 ) ) )
56 5 54 12 15 55 syl13anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) 𝑌 ) ↔ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 𝑌 ) ) )
57 44 52 56 mpbi2and ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 𝑌 ) )
58 1 4 3 lautle ( ( ( 𝐾 ∈ Lat ∧ 𝐹𝐼 ) ∧ ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ∈ 𝐵 ∧ ( 𝑋 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ) )
59 7 54 9 58 syl12anc ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ( le ‘ 𝐾 ) ( 𝑋 𝑌 ) ↔ ( 𝐹 ‘ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 𝑌 ) ) ) )
60 57 59 mpbid ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 𝑌 ) ) )
61 36 60 eqbrtrrd ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 𝑌 ) ) )
62 1 4 5 11 19 32 61 latasymd ( ( 𝐾 ∈ Lat ∧ ( 𝐹𝐼𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )