Metamath Proof Explorer

Theorem lautj

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

Ref Expression
Hypotheses lautj.b ⊢B=BaseK
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=BaseK
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 ontoB
21 20 3ad2antr1 ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F:B⟶1-1 ontoB
22 f1ocnvfv1 ⊢F:B⟶1-1 ontoB∧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≤KF⁡X∨˙F⁡Y
25 5 14 17 24 syl3anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X≤KF⁡X∨˙F⁡Y
26 f1ocnvfv2 ⊢F:B⟶1-1 ontoB∧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≤KF⁡F-1⁡F⁡X∨˙F⁡Y
29 f1ocnvdm ⊢F:B⟶1-1 ontoB∧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≤KF-1⁡F⁡X∨˙F⁡Y↔F⁡X≤KF⁡F-1⁡F⁡X∨˙F⁡Y
32 7 12 30 31 syl12anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X≤KF-1⁡F⁡X∨˙F⁡Y↔F⁡X≤KF⁡F-1⁡F⁡X∨˙F⁡Y
33 28 32 mpbird ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X≤KF-1⁡F⁡X∨˙F⁡Y
34 1 4 2 latlej2 ⊢K∈Lat∧F⁡X∈B∧F⁡Y∈B→F⁡Y≤KF⁡X∨˙F⁡Y
35 5 14 17 34 syl3anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡Y≤KF⁡X∨˙F⁡Y
36 35 27 breqtrrd ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡Y≤KF⁡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≤KF-1⁡F⁡X∨˙F⁡Y↔F⁡Y≤KF⁡F-1⁡F⁡X∨˙F⁡Y
38 7 15 30 37 syl12anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→Y≤KF-1⁡F⁡X∨˙F⁡Y↔F⁡Y≤KF⁡F-1⁡F⁡X∨˙F⁡Y
39 36 38 mpbird ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→Y≤KF-1⁡F⁡X∨˙F⁡Y
40 1 4 2 latjle12 ⊢K∈Lat∧X∈B∧Y∈B∧F-1⁡F⁡X∨˙F⁡Y∈B→X≤KF-1⁡F⁡X∨˙F⁡Y∧Y≤KF-1⁡F⁡X∨˙F⁡Y↔X∨˙Y≤KF-1⁡F⁡X∨˙F⁡Y
41 5 12 15 30 40 syl13anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X≤KF-1⁡F⁡X∨˙F⁡Y∧Y≤KF-1⁡F⁡X∨˙F⁡Y↔X∨˙Y≤KF-1⁡F⁡X∨˙F⁡Y
42 33 39 41 mpbi2and ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X∨˙Y≤KF-1⁡F⁡X∨˙F⁡Y
43 23 42 eqbrtrd ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F-1⁡F⁡X∨˙Y≤KF-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≤KF⁡X∨˙F⁡Y↔F-1⁡F⁡X∨˙Y≤KF-1⁡F⁡X∨˙F⁡Y
45 7 11 19 44 syl12anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X∨˙Y≤KF⁡X∨˙F⁡Y↔F-1⁡F⁡X∨˙Y≤KF-1⁡F⁡X∨˙F⁡Y
46 43 45 mpbird ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X∨˙Y≤KF⁡X∨˙F⁡Y
47 1 4 2 latlej1 ⊢K∈Lat∧X∈B∧Y∈B→X≤KX∨˙Y
48 47 3adant3r1 ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X≤KX∨˙Y
49 1 4 3 lautle ⊢K∈Lat∧F∈I∧X∈B∧X∨˙Y∈B→X≤KX∨˙Y↔F⁡X≤KF⁡X∨˙Y
50 7 12 9 49 syl12anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→X≤KX∨˙Y↔F⁡X≤KF⁡X∨˙Y
51 48 50 mpbid ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X≤KF⁡X∨˙Y
52 1 4 2 latlej2 ⊢K∈Lat∧X∈B∧Y∈B→Y≤KX∨˙Y
53 52 3adant3r1 ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→Y≤KX∨˙Y
54 1 4 3 lautle ⊢K∈Lat∧F∈I∧Y∈B∧X∨˙Y∈B→Y≤KX∨˙Y↔F⁡Y≤KF⁡X∨˙Y
55 7 15 9 54 syl12anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→Y≤KX∨˙Y↔F⁡Y≤KF⁡X∨˙Y
56 53 55 mpbid ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡Y≤KF⁡X∨˙Y
57 1 4 2 latjle12 ⊢K∈Lat∧F⁡X∈B∧F⁡Y∈B∧F⁡X∨˙Y∈B→F⁡X≤KF⁡X∨˙Y∧F⁡Y≤KF⁡X∨˙Y↔F⁡X∨˙F⁡Y≤KF⁡X∨˙Y
58 5 14 17 11 57 syl13anc ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X≤KF⁡X∨˙Y∧F⁡Y≤KF⁡X∨˙Y↔F⁡X∨˙F⁡Y≤KF⁡X∨˙Y
59 51 56 58 mpbi2and ⊢K∈Lat∧F∈I∧X∈B∧Y∈B→F⁡X∨˙F⁡Y≤KF⁡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