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