Metamath Proof Explorer


Theorem lautm

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

Ref Expression
Hypotheses lautm.b B=BaseK
lautm.m ˙=meetK
lautm.i I=LAutK
Assertion lautm KLatFIXBYBFX˙Y=FX˙FY

Proof

Step Hyp Ref Expression
1 lautm.b B=BaseK
2 lautm.m ˙=meetK
3 lautm.i I=LAutK
4 eqid K=K
5 simpl KLatFIXBYBKLat
6 simpr1 KLatFIXBYBFI
7 5 6 jca KLatFIXBYBKLatFI
8 1 2 latmcl KLatXBYBX˙YB
9 8 3adant3r1 KLatFIXBYBX˙YB
10 1 3 lautcl KLatFIX˙YBFX˙YB
11 7 9 10 syl2anc KLatFIXBYBFX˙YB
12 simpr2 KLatFIXBYBXB
13 1 3 lautcl KLatFIXBFXB
14 7 12 13 syl2anc KLatFIXBYBFXB
15 simpr3 KLatFIXBYBYB
16 1 3 lautcl KLatFIYBFYB
17 7 15 16 syl2anc KLatFIXBYBFYB
18 1 2 latmcl KLatFXBFYBFX˙FYB
19 5 14 17 18 syl3anc KLatFIXBYBFX˙FYB
20 1 4 2 latmle1 KLatXBYBX˙YKX
21 20 3adant3r1 KLatFIXBYBX˙YKX
22 1 4 3 lautle KLatFIX˙YBXBX˙YKXFX˙YKFX
23 7 9 12 22 syl12anc KLatFIXBYBX˙YKXFX˙YKFX
24 21 23 mpbid KLatFIXBYBFX˙YKFX
25 1 4 2 latmle2 KLatXBYBX˙YKY
26 25 3adant3r1 KLatFIXBYBX˙YKY
27 1 4 3 lautle KLatFIX˙YBYBX˙YKYFX˙YKFY
28 7 9 15 27 syl12anc KLatFIXBYBX˙YKYFX˙YKFY
29 26 28 mpbid KLatFIXBYBFX˙YKFY
30 1 4 2 latlem12 KLatFX˙YBFXBFYBFX˙YKFXFX˙YKFYFX˙YKFX˙FY
31 5 11 14 17 30 syl13anc KLatFIXBYBFX˙YKFXFX˙YKFYFX˙YKFX˙FY
32 24 29 31 mpbi2and KLatFIXBYBFX˙YKFX˙FY
33 1 3 laut1o KLatFIF:B1-1 ontoB
34 33 3ad2antr1 KLatFIXBYBF:B1-1 ontoB
35 f1ocnvfv2 F:B1-1 ontoBFX˙FYBFF-1FX˙FY=FX˙FY
36 34 19 35 syl2anc KLatFIXBYBFF-1FX˙FY=FX˙FY
37 1 4 2 latmle1 KLatFXBFYBFX˙FYKFX
38 5 14 17 37 syl3anc KLatFIXBYBFX˙FYKFX
39 1 4 3 lautcnvle KLatFIFX˙FYBFXBFX˙FYKFXF-1FX˙FYKF-1FX
40 7 19 14 39 syl12anc KLatFIXBYBFX˙FYKFXF-1FX˙FYKF-1FX
41 38 40 mpbid KLatFIXBYBF-1FX˙FYKF-1FX
42 f1ocnvfv1 F:B1-1 ontoBXBF-1FX=X
43 34 12 42 syl2anc KLatFIXBYBF-1FX=X
44 41 43 breqtrd KLatFIXBYBF-1FX˙FYKX
45 1 4 2 latmle2 KLatFXBFYBFX˙FYKFY
46 5 14 17 45 syl3anc KLatFIXBYBFX˙FYKFY
47 1 4 3 lautcnvle KLatFIFX˙FYBFYBFX˙FYKFYF-1FX˙FYKF-1FY
48 7 19 17 47 syl12anc KLatFIXBYBFX˙FYKFYF-1FX˙FYKF-1FY
49 46 48 mpbid KLatFIXBYBF-1FX˙FYKF-1FY
50 f1ocnvfv1 F:B1-1 ontoBYBF-1FY=Y
51 34 15 50 syl2anc KLatFIXBYBF-1FY=Y
52 49 51 breqtrd KLatFIXBYBF-1FX˙FYKY
53 f1ocnvdm F:B1-1 ontoBFX˙FYBF-1FX˙FYB
54 34 19 53 syl2anc KLatFIXBYBF-1FX˙FYB
55 1 4 2 latlem12 KLatF-1FX˙FYBXBYBF-1FX˙FYKXF-1FX˙FYKYF-1FX˙FYKX˙Y
56 5 54 12 15 55 syl13anc KLatFIXBYBF-1FX˙FYKXF-1FX˙FYKYF-1FX˙FYKX˙Y
57 44 52 56 mpbi2and KLatFIXBYBF-1FX˙FYKX˙Y
58 1 4 3 lautle KLatFIF-1FX˙FYBX˙YBF-1FX˙FYKX˙YFF-1FX˙FYKFX˙Y
59 7 54 9 58 syl12anc KLatFIXBYBF-1FX˙FYKX˙YFF-1FX˙FYKFX˙Y
60 57 59 mpbid KLatFIXBYBFF-1FX˙FYKFX˙Y
61 36 60 eqbrtrrd KLatFIXBYBFX˙FYKFX˙Y
62 1 4 5 11 19 32 61 latasymd KLatFIXBYBFX˙Y=FX˙FY