Description: Version of modular law pmod1i that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012) (Revised by Mario Carneiro, 10-May-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atmod.b | |
|
atmod.l | |
||
atmod.j | |
||
atmod.m | |
||
atmod.a | |
||
Assertion | atmod1i1m | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atmod.b | |
|
2 | atmod.l | |
|
3 | atmod.j | |
|
4 | atmod.m | |
|
5 | atmod.a | |
|
6 | simpl1l | |
|
7 | simpr | |
|
8 | simpl22 | |
|
9 | simpl23 | |
|
10 | simpl3 | |
|
11 | 1 2 3 4 5 | atmod1i1 | |
12 | 6 7 8 9 10 11 | syl131anc | |
13 | simp1l | |
|
14 | hlol | |
|
15 | 13 14 | syl | |
16 | 15 | adantr | |
17 | 13 | hllatd | |
18 | 17 | adantr | |
19 | simpl22 | |
|
20 | simpl23 | |
|
21 | 1 4 | latmcl | |
22 | 18 19 20 21 | syl3anc | |
23 | eqid | |
|
24 | 1 3 23 | olj02 | |
25 | 16 22 24 | syl2anc | |
26 | oveq1 | |
|
27 | 26 | adantl | |
28 | oveq1 | |
|
29 | 28 | adantl | |
30 | 1 3 23 | olj02 | |
31 | 16 19 30 | syl2anc | |
32 | 29 31 | eqtrd | |
33 | 32 | oveq1d | |
34 | 25 27 33 | 3eqtr4d | |
35 | simp21 | |
|
36 | simp1r | |
|
37 | 1 4 23 5 | meetat2 | |
38 | 15 35 36 37 | syl3anc | |
39 | 12 34 38 | mpjaodan | |