Metamath Proof Explorer


Theorem cdleme50laut

Description: Part of proof of Lemma D in Crawley p. 113. F is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B=BaseK
cdlemef50.l ˙=K
cdlemef50.j ˙=joinK
cdlemef50.m ˙=meetK
cdlemef50.a A=AtomsK
cdlemef50.h H=LHypK
cdlemef50.u U=P˙Q˙W
cdlemef50.d D=t˙U˙Q˙P˙t˙W
cdlemefs50.e E=P˙Q˙D˙s˙t˙W
cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
cdleme50laut.i I=LAutK
Assertion cdleme50laut KHLWHPA¬P˙WQA¬Q˙WFI

Proof

Step Hyp Ref Expression
1 cdlemef50.b B=BaseK
2 cdlemef50.l ˙=K
3 cdlemef50.j ˙=joinK
4 cdlemef50.m ˙=meetK
5 cdlemef50.a A=AtomsK
6 cdlemef50.h H=LHypK
7 cdlemef50.u U=P˙Q˙W
8 cdlemef50.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs50.e E=P˙Q˙D˙s˙t˙W
10 cdlemef50.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 cdleme50laut.i I=LAutK
12 1 2 3 4 5 6 7 8 9 10 cdleme50f1o KHLWHPA¬P˙WQA¬Q˙WF:B1-1 ontoB
13 1 2 3 4 5 6 7 8 9 10 cdleme50lebi KHLWHPA¬P˙WQA¬Q˙WdBeBd˙eFd˙Fe
14 13 ralrimivva KHLWHPA¬P˙WQA¬Q˙WdBeBd˙eFd˙Fe
15 simp1l KHLWHPA¬P˙WQA¬Q˙WKHL
16 1 2 11 islaut KHLFIF:B1-1 ontoBdBeBd˙eFd˙Fe
17 15 16 syl KHLWHPA¬P˙WQA¬Q˙WFIF:B1-1 ontoBdBeBd˙eFd˙Fe
18 12 14 17 mpbir2and KHLWHPA¬P˙WQA¬Q˙WFI