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 | |
|
lhpelim.l | |
||
lhpelim.j | |
||
lhpelim.m | |
||
lhpelim.a | |
||
lhpelim.h | |
||
Assertion | lhpelim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpelim.b | |
|
2 | lhpelim.l | |
|
3 | lhpelim.j | |
|
4 | lhpelim.m | |
|
5 | lhpelim.a | |
|
6 | lhpelim.h | |
|
7 | eqid | |
|
8 | 2 4 7 5 6 | lhpmat | |
9 | 8 | 3adant3 | |
10 | 9 | oveq1d | |
11 | simp1l | |
|
12 | simp2l | |
|
13 | 11 | hllatd | |
14 | simp3 | |
|
15 | simp1r | |
|
16 | 1 6 | lhpbase | |
17 | 15 16 | syl | |
18 | 1 4 | latmcl | |
19 | 13 14 17 18 | syl3anc | |
20 | 1 2 4 | latmle2 | |
21 | 13 14 17 20 | syl3anc | |
22 | 1 2 3 4 5 | atmod4i2 | |
23 | 11 12 19 17 21 22 | syl131anc | |
24 | hlol | |
|
25 | 11 24 | syl | |
26 | 1 3 7 | olj02 | |
27 | 25 19 26 | syl2anc | |
28 | 10 23 27 | 3eqtr3d | |