Description: Version of modular law pmod2iN that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012) (Revised by Mario Carneiro, 10-May-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atmod.b | |
|
atmod.l | |
||
atmod.j | |
||
atmod.m | |
||
atmod.a | |
||
Assertion | atmod2i1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atmod.b | |
|
2 | atmod.l | |
|
3 | atmod.j | |
|
4 | atmod.m | |
|
5 | atmod.a | |
|
6 | hllat | |
|
7 | 6 | 3ad2ant1 | |
8 | simp22 | |
|
9 | simp23 | |
|
10 | 1 4 | latmcom | |
11 | 7 8 9 10 | syl3anc | |
12 | 11 | oveq2d | |
13 | simp21 | |
|
14 | 1 5 | atbase | |
15 | 13 14 | syl | |
16 | 1 4 | latmcl | |
17 | 7 8 9 16 | syl3anc | |
18 | 1 3 | latjcom | |
19 | 7 15 17 18 | syl3anc | |
20 | 1 3 | latjcl | |
21 | 7 15 9 20 | syl3anc | |
22 | 1 4 | latmcom | |
23 | 7 21 8 22 | syl3anc | |
24 | simp1 | |
|
25 | simp3 | |
|
26 | 1 2 3 4 5 | atmod1i1 | |
27 | 24 13 9 8 25 26 | syl131anc | |
28 | 1 3 | latjcom | |
29 | 7 9 15 28 | syl3anc | |
30 | 29 | oveq2d | |
31 | 23 27 30 | 3eqtr4d | |
32 | 12 19 31 | 3eqtr3d | |