Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 18-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhpjat.l | |
|
lhpjat.j | |
||
lhpjat.u | |
||
lhpjat.a | |
||
lhpjat.h | |
||
Assertion | lhpjat1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhpjat.l | |
|
2 | lhpjat.j | |
|
3 | lhpjat.u | |
|
4 | lhpjat.a | |
|
5 | lhpjat.h | |
|
6 | simpll | |
|
7 | eqid | |
|
8 | 7 5 | lhpbase | |
9 | 8 | ad2antlr | |
10 | simprl | |
|
11 | eqid | |
|
12 | 3 11 5 | lhp1cvr | |
13 | 12 | adantr | |
14 | simprr | |
|
15 | 7 1 2 3 11 4 | 1cvrjat | |
16 | 6 9 10 13 14 15 | syl32anc | |