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 Lat F I X B Y 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 K = K
5 simpl K Lat F I X B Y B K Lat
6 simpr1 K Lat F I X B Y B F I
7 5 6 jca K Lat F I X B Y B K Lat F I
8 1 2 latjcl K Lat X B Y B X ˙ Y B
9 8 3adant3r1 K Lat F I X B Y B X ˙ Y B
10 1 3 lautcl K Lat F I X ˙ Y B F X ˙ Y B
11 7 9 10 syl2anc K Lat F I X B Y B F X ˙ Y B
12 simpr2 K Lat F I X B Y B X B
13 1 3 lautcl K Lat F I X B F X B
14 7 12 13 syl2anc K Lat F I X B Y B F X B
15 simpr3 K Lat F I X B Y B Y B
16 1 3 lautcl K Lat F I Y B F Y B
17 7 15 16 syl2anc K Lat F I X B Y B F Y B
18 1 2 latjcl K Lat F X B F Y B F X ˙ F Y B
19 5 14 17 18 syl3anc K Lat F I X B Y B F X ˙ F Y B
20 1 3 laut1o K Lat F I F : B 1-1 onto B
21 20 3ad2antr1 K Lat F I X B Y B F : B 1-1 onto B
22 f1ocnvfv1 F : B 1-1 onto B X ˙ Y B F -1 F X ˙ Y = X ˙ Y
23 21 9 22 syl2anc K Lat F I X B Y B F -1 F X ˙ Y = X ˙ Y
24 1 4 2 latlej1 K Lat F X B F Y B F X K F X ˙ F Y
25 5 14 17 24 syl3anc K Lat F I X B Y B F X K F X ˙ F Y
26 f1ocnvfv2 F : B 1-1 onto B F X ˙ F Y B F F -1 F X ˙ F Y = F X ˙ F Y
27 21 19 26 syl2anc K Lat F I X B Y B F F -1 F X ˙ F Y = F X ˙ F Y
28 25 27 breqtrrd K Lat F I X B Y B F X K F F -1 F X ˙ F Y
29 f1ocnvdm F : B 1-1 onto B F X ˙ F Y B F -1 F X ˙ F Y B
30 21 19 29 syl2anc K Lat F I X B Y B F -1 F X ˙ F Y B
31 1 4 3 lautle K Lat F I X B F -1 F X ˙ F Y B X K F -1 F X ˙ F Y F X K F F -1 F X ˙ F Y
32 7 12 30 31 syl12anc K Lat F I X B Y B X K F -1 F X ˙ F Y F X K F F -1 F X ˙ F Y
33 28 32 mpbird K Lat F I X B Y B X K F -1 F X ˙ F Y
34 1 4 2 latlej2 K Lat F X B F Y B F Y K F X ˙ F Y
35 5 14 17 34 syl3anc K Lat F I X B Y B F Y K F X ˙ F Y
36 35 27 breqtrrd K Lat F I X B Y B F Y K F F -1 F X ˙ F Y
37 1 4 3 lautle K Lat F I Y B F -1 F X ˙ F Y B Y K F -1 F X ˙ F Y F Y K F F -1 F X ˙ F Y
38 7 15 30 37 syl12anc K Lat F I X B Y B Y K F -1 F X ˙ F Y F Y K F F -1 F X ˙ F Y
39 36 38 mpbird K Lat F I X B Y B Y K F -1 F X ˙ F Y
40 1 4 2 latjle12 K Lat X B Y B F -1 F X ˙ F Y B X K F -1 F X ˙ F Y Y K F -1 F X ˙ F Y X ˙ Y K F -1 F X ˙ F Y
41 5 12 15 30 40 syl13anc K Lat F I X B Y B X K F -1 F X ˙ F Y Y K F -1 F X ˙ F Y X ˙ Y K F -1 F X ˙ F Y
42 33 39 41 mpbi2and K Lat F I X B Y B X ˙ Y K F -1 F X ˙ F Y
43 23 42 eqbrtrd K Lat F I X B Y B F -1 F X ˙ Y K F -1 F X ˙ F Y
44 1 4 3 lautcnvle K Lat F I F X ˙ Y B F X ˙ F Y B F X ˙ Y K F X ˙ F Y F -1 F X ˙ Y K F -1 F X ˙ F Y
45 7 11 19 44 syl12anc K Lat F I X B Y B F X ˙ Y K F X ˙ F Y F -1 F X ˙ Y K F -1 F X ˙ F Y
46 43 45 mpbird K Lat F I X B Y B F X ˙ Y K F X ˙ F Y
47 1 4 2 latlej1 K Lat X B Y B X K X ˙ Y
48 47 3adant3r1 K Lat F I X B Y B X K X ˙ Y
49 1 4 3 lautle K Lat F I X B X ˙ Y B X K X ˙ Y F X K F X ˙ Y
50 7 12 9 49 syl12anc K Lat F I X B Y B X K X ˙ Y F X K F X ˙ Y
51 48 50 mpbid K Lat F I X B Y B F X K F X ˙ Y
52 1 4 2 latlej2 K Lat X B Y B Y K X ˙ Y
53 52 3adant3r1 K Lat F I X B Y B Y K X ˙ Y
54 1 4 3 lautle K Lat F I Y B X ˙ Y B Y K X ˙ Y F Y K F X ˙ Y
55 7 15 9 54 syl12anc K Lat F I X B Y B Y K X ˙ Y F Y K F X ˙ Y
56 53 55 mpbid K Lat F I X B Y B F Y K F X ˙ Y
57 1 4 2 latjle12 K Lat F X B F Y B F X ˙ Y B F X K F X ˙ Y F Y K F X ˙ Y F X ˙ F Y K F X ˙ Y
58 5 14 17 11 57 syl13anc K Lat F I X B Y B F X K F X ˙ Y F Y K F X ˙ Y F X ˙ F Y K F X ˙ Y
59 51 56 58 mpbi2and K Lat F I X B Y B F X ˙ F Y K F X ˙ Y
60 1 4 5 11 19 46 59 latasymd K Lat F I X B Y B F X ˙ Y = F X ˙ F Y