Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihjatcclem.b | |
|
dihjatcclem.l | |
||
dihjatcclem.h | |
||
dihjatcclem.j | |
||
dihjatcclem.m | |
||
dihjatcclem.a | |
||
dihjatcclem.u | |
||
dihjatcclem.s | |
||
dihjatcclem.i | |
||
dihjatcclem.v | |
||
dihjatcclem.k | |
||
dihjatcclem.p | |
||
dihjatcclem.q | |
||
dihjatcclem2.c | |
||
Assertion | dihjatcclem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihjatcclem.b | |
|
2 | dihjatcclem.l | |
|
3 | dihjatcclem.h | |
|
4 | dihjatcclem.j | |
|
5 | dihjatcclem.m | |
|
6 | dihjatcclem.a | |
|
7 | dihjatcclem.u | |
|
8 | dihjatcclem.s | |
|
9 | dihjatcclem.i | |
|
10 | dihjatcclem.v | |
|
11 | dihjatcclem.k | |
|
12 | dihjatcclem.p | |
|
13 | dihjatcclem.q | |
|
14 | dihjatcclem2.c | |
|
15 | 1 2 3 4 5 6 7 8 9 10 11 12 13 | dihjatcclem1 | |
16 | 3 7 11 | dvhlmod | |
17 | eqid | |
|
18 | 17 | lsssssubg | |
19 | 16 18 | syl | |
20 | 12 | simpld | |
21 | 1 6 | atbase | |
22 | 20 21 | syl | |
23 | 1 3 9 7 17 | dihlss | |
24 | 11 22 23 | syl2anc | |
25 | 13 | simpld | |
26 | 1 6 | atbase | |
27 | 25 26 | syl | |
28 | 1 3 9 7 17 | dihlss | |
29 | 11 27 28 | syl2anc | |
30 | 17 8 | lsmcl | |
31 | 16 24 29 30 | syl3anc | |
32 | 19 31 | sseldd | |
33 | 10 | fveq2i | |
34 | 11 | simpld | |
35 | 34 | hllatd | |
36 | 1 4 6 | hlatjcl | |
37 | 34 20 25 36 | syl3anc | |
38 | 11 | simprd | |
39 | 1 3 | lhpbase | |
40 | 38 39 | syl | |
41 | 1 5 | latmcl | |
42 | 35 37 40 41 | syl3anc | |
43 | 1 3 9 7 17 | dihlss | |
44 | 11 42 43 | syl2anc | |
45 | 33 44 | eqeltrid | |
46 | 19 45 | sseldd | |
47 | 8 | lsmss2 | |
48 | 32 46 14 47 | syl3anc | |
49 | 15 48 | eqtrd | |