Metamath Proof Explorer

Theorem lautm

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

Ref Expression
Hypotheses lautm.b 
|- B = ( Base ` K )
lautm.m 
|- ./\ = ( meet ` K )
lautm.i 
|- I = ( LAut ` K )
Assertion lautm 
|- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) )

Proof

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