Metamath Proof Explorer


Theorem cdlemc1

Description: Part of proof of Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemc1.b B=BaseK
cdlemc1.l ˙=K
cdlemc1.j ˙=joinK
cdlemc1.m ˙=meetK
cdlemc1.a A=AtomsK
cdlemc1.h H=LHypK
Assertion cdlemc1 KHLWHXBPA¬P˙WP˙P˙X˙W=P˙X

Proof

Step Hyp Ref Expression
1 cdlemc1.b B=BaseK
2 cdlemc1.l ˙=K
3 cdlemc1.j ˙=joinK
4 cdlemc1.m ˙=meetK
5 cdlemc1.a A=AtomsK
6 cdlemc1.h H=LHypK
7 simp1l KHLWHXBPA¬P˙WKHL
8 7 hllatd KHLWHXBPA¬P˙WKLat
9 simp3l KHLWHXBPA¬P˙WPA
10 1 5 atbase PAPB
11 9 10 syl KHLWHXBPA¬P˙WPB
12 simp2 KHLWHXBPA¬P˙WXB
13 1 3 latjcl KLatPBXBP˙XB
14 8 11 12 13 syl3anc KHLWHXBPA¬P˙WP˙XB
15 simp1r KHLWHXBPA¬P˙WWH
16 1 6 lhpbase WHWB
17 15 16 syl KHLWHXBPA¬P˙WWB
18 1 4 latmcl KLatP˙XBWBP˙X˙WB
19 8 14 17 18 syl3anc KHLWHXBPA¬P˙WP˙X˙WB
20 1 3 latjcom KLatPBP˙X˙WBP˙P˙X˙W=P˙X˙W˙P
21 8 11 19 20 syl3anc KHLWHXBPA¬P˙WP˙P˙X˙W=P˙X˙W˙P
22 1 2 3 latlej1 KLatPBXBP˙P˙X
23 8 11 12 22 syl3anc KHLWHXBPA¬P˙WP˙P˙X
24 1 2 3 4 5 atmod2i1 KHLPAP˙XBWBP˙P˙XP˙X˙W˙P=P˙X˙W˙P
25 7 9 14 17 23 24 syl131anc KHLWHXBPA¬P˙WP˙X˙W˙P=P˙X˙W˙P
26 eqid 1.K=1.K
27 2 3 26 5 6 lhpjat1 KHLWHPA¬P˙WW˙P=1.K
28 27 3adant2 KHLWHXBPA¬P˙WW˙P=1.K
29 28 oveq2d KHLWHXBPA¬P˙WP˙X˙W˙P=P˙X˙1.K
30 hlol KHLKOL
31 7 30 syl KHLWHXBPA¬P˙WKOL
32 1 4 26 olm11 KOLP˙XBP˙X˙1.K=P˙X
33 31 14 32 syl2anc KHLWHXBPA¬P˙WP˙X˙1.K=P˙X
34 29 33 eqtrd KHLWHXBPA¬P˙WP˙X˙W˙P=P˙X
35 21 25 34 3eqtrd KHLWHXBPA¬P˙WP˙P˙X˙W=P˙X