Description: The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2atjm.b | |
|
2atjm.l | |
||
2atjm.j | |
||
2atjm.m | |
||
2atjm.a | |
||
Assertion | 2atjm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2atjm.b | |
|
2 | 2atjm.l | |
|
3 | 2atjm.j | |
|
4 | 2atjm.m | |
|
5 | 2atjm.a | |
|
6 | hllat | |
|
7 | 6 | 3ad2ant1 | |
8 | simp21 | |
|
9 | 1 5 | atbase | |
10 | 8 9 | syl | |
11 | simp22 | |
|
12 | 1 5 | atbase | |
13 | 11 12 | syl | |
14 | 1 2 3 | latlej1 | |
15 | 7 10 13 14 | syl3anc | |
16 | simp3l | |
|
17 | simp1 | |
|
18 | 1 3 5 | hlatjcl | |
19 | 17 8 11 18 | syl3anc | |
20 | simp23 | |
|
21 | 1 2 4 | latlem12 | |
22 | 7 10 19 20 21 | syl13anc | |
23 | 15 16 22 | mpbi2and | |
24 | hlatl | |
|
25 | 24 | 3ad2ant1 | |
26 | 1 4 | latmcom | |
27 | 7 19 20 26 | syl3anc | |
28 | 20 8 11 | 3jca | |
29 | nbrne2 | |
|
30 | 29 | 3ad2ant3 | |
31 | simp3r | |
|
32 | 1 3 | latjcl | |
33 | 7 20 13 32 | syl3anc | |
34 | 1 2 3 | latlej1 | |
35 | 7 20 13 34 | syl3anc | |
36 | 1 2 7 10 20 33 16 35 | lattrd | |
37 | 1 2 3 4 5 | cvrat3 | |
38 | 37 | imp | |
39 | 17 28 30 31 36 38 | syl23anc | |
40 | 27 39 | eqeltrd | |
41 | 2 5 | atcmp | |
42 | 25 8 40 41 | syl3anc | |
43 | 23 42 | mpbid | |
44 | 43 | eqcomd | |