Metamath Proof Explorer

Theorem lautj

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

Ref Expression
Hypotheses lautj.b 
|- B = ( Base ` K )
lautj.j 
|- .\/ = ( join ` K )
lautj.i 
|- I = ( LAut ` K )
Assertion lautj 
|- ( ( 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 lautj.b 
 |-  B = ( Base ` K )
2 lautj.j 
 |-  .\/ = ( join ` K )
3 lautj.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 latjcl 
 |-  ( ( 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 latjcl 
 |-  ( ( 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 3 laut1o 
 |-  ( ( K e. Lat /\ F e. I ) -> F : B -1-1-onto-> B )
21 20 3ad2antr1 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> F : B -1-1-onto-> B )
22 f1ocnvfv1 
 |-  ( ( F : B -1-1-onto-> B /\ ( X .\/ Y ) e. B ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) = ( X .\/ Y ) )
23 21 9 22 syl2anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) = ( X .\/ Y ) )
24 1 4 2 latlej1 
 |-  ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( F ` X ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) )
25 5 14 17 24 syl3anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) )
26 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) -> ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )
27 21 19 26 syl2anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )
28 25 27 breqtrrd 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
29 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) -> ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B )
30 21 19 29 syl2anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B )
31 1 4 3 lautle 
 |-  ( ( ( K e. Lat /\ F e. I ) /\ ( X e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) )
32 7 12 30 31 syl12anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` X ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) )
33 28 32 mpbird 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) )
34 1 4 2 latlej2 
 |-  ( ( K e. Lat /\ ( F ` X ) e. B /\ ( F ` Y ) e. B ) -> ( F ` Y ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) )
35 5 14 17 34 syl3anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) )
36 35 27 breqtrrd 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
37 1 4 3 lautle 
 |-  ( ( ( K e. Lat /\ F e. I ) /\ ( Y e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) )
38 7 15 30 37 syl12anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) <-> ( F ` Y ) ( le ` K ) ( F ` ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) ) )
39 36 38 mpbird 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) )
40 1 4 2 latjle12 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) e. B ) ) -> ( ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) /\ Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
41 5 12 15 30 40 syl13anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( X ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) /\ Y ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) <-> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
42 33 39 41 mpbi2and 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X .\/ Y ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) )
43 23 42 eqbrtrd 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) )
44 1 4 3 lautcnvle 
 |-  ( ( ( K e. Lat /\ F e. I ) /\ ( ( F ` ( X .\/ Y ) ) e. B /\ ( ( F ` X ) .\/ ( F ` Y ) ) e. B ) ) -> ( ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) <-> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
45 7 11 19 44 syl12anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) <-> ( `' F ` ( F ` ( X .\/ Y ) ) ) ( le ` K ) ( `' F ` ( ( F ` X ) .\/ ( F ` Y ) ) ) ) )
46 43 45 mpbird 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) ( le ` K ) ( ( F ` X ) .\/ ( F ` Y ) ) )
47 1 4 2 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X ( le ` K ) ( X .\/ Y ) )
48 47 3adant3r1 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> X ( le ` K ) ( X .\/ Y ) )
49 1 4 3 lautle 
 |-  ( ( ( K e. Lat /\ F e. I ) /\ ( X e. B /\ ( X .\/ Y ) e. B ) ) -> ( X ( le ` K ) ( X .\/ Y ) <-> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
50 7 12 9 49 syl12anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X ( le ` K ) ( X .\/ Y ) <-> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
51 48 50 mpbid 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) )
52 1 4 2 latlej2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y ( le ` K ) ( X .\/ Y ) )
53 52 3adant3r1 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> Y ( le ` K ) ( X .\/ Y ) )
54 1 4 3 lautle 
 |-  ( ( ( K e. Lat /\ F e. I ) /\ ( Y e. B /\ ( X .\/ Y ) e. B ) ) -> ( Y ( le ` K ) ( X .\/ Y ) <-> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
55 7 15 9 54 syl12anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( Y ( le ` K ) ( X .\/ Y ) <-> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
56 53 55 mpbid 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) )
57 1 4 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( F ` X ) e. B /\ ( F ` Y ) e. B /\ ( F ` ( X .\/ Y ) ) e. B ) ) -> ( ( ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) /\ ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) <-> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
58 5 14 17 11 57 syl13anc 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( ( F ` X ) ( le ` K ) ( F ` ( X .\/ Y ) ) /\ ( F ` Y ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) <-> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) ) )
59 51 56 58 mpbi2and 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( ( F ` X ) .\/ ( F ` Y ) ) ( le ` K ) ( F ` ( X .\/ Y ) ) )
60 1 4 5 11 19 46 59 latasymd 
 |-  ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )