Metamath Proof Explorer


Theorem lhpelim

Description: Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 lhpelim.b B=BaseK
2 lhpelim.l ˙=K
3 lhpelim.j ˙=joinK
4 lhpelim.m ˙=meetK
5 lhpelim.a A=AtomsK
6 lhpelim.h H=LHypK
7 eqid 0.K=0.K
8 2 4 7 5 6 lhpmat KHLWHPA¬P˙WP˙W=0.K
9 8 3adant3 KHLWHPA¬P˙WXBP˙W=0.K
10 9 oveq1d KHLWHPA¬P˙WXBP˙W˙X˙W=0.K˙X˙W
11 simp1l KHLWHPA¬P˙WXBKHL
12 simp2l KHLWHPA¬P˙WXBPA
13 11 hllatd KHLWHPA¬P˙WXBKLat
14 simp3 KHLWHPA¬P˙WXBXB
15 simp1r KHLWHPA¬P˙WXBWH
16 1 6 lhpbase WHWB
17 15 16 syl KHLWHPA¬P˙WXBWB
18 1 4 latmcl KLatXBWBX˙WB
19 13 14 17 18 syl3anc KHLWHPA¬P˙WXBX˙WB
20 1 2 4 latmle2 KLatXBWBX˙W˙W
21 13 14 17 20 syl3anc KHLWHPA¬P˙WXBX˙W˙W
22 1 2 3 4 5 atmod4i2 KHLPAX˙WBWBX˙W˙WP˙W˙X˙W=P˙X˙W˙W
23 11 12 19 17 21 22 syl131anc KHLWHPA¬P˙WXBP˙W˙X˙W=P˙X˙W˙W
24 hlol KHLKOL
25 11 24 syl KHLWHPA¬P˙WXBKOL
26 1 3 7 olj02 KOLX˙WB0.K˙X˙W=X˙W
27 25 19 26 syl2anc KHLWHPA¬P˙WXB0.K˙X˙W=X˙W
28 10 23 27 3eqtr3d KHLWHPA¬P˙WXBP˙X˙W˙W=X˙W