Description: Orthomodular law equivalent. Remark in Holland95 p. 223. (Contributed by NM, 19-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omllaw4.b | |
|
omllaw4.l | |
||
omllaw4.m | |
||
omllaw4.o | |
||
Assertion | omllaw4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omllaw4.b | |
|
2 | omllaw4.l | |
|
3 | omllaw4.m | |
|
4 | omllaw4.o | |
|
5 | simp1 | |
|
6 | omlop | |
|
7 | 6 | 3ad2ant1 | |
8 | simp3 | |
|
9 | 1 4 | opoccl | |
10 | 7 8 9 | syl2anc | |
11 | simp2 | |
|
12 | 1 4 | opoccl | |
13 | 7 11 12 | syl2anc | |
14 | eqid | |
|
15 | 1 2 14 3 4 | omllaw | |
16 | 5 10 13 15 | syl3anc | |
17 | 1 2 4 | oplecon3b | |
18 | 6 17 | syl3an1 | |
19 | omllat | |
|
20 | 19 | 3ad2ant1 | |
21 | 1 3 | latmcl | |
22 | 20 13 8 21 | syl3anc | |
23 | 1 4 | opoccl | |
24 | 7 22 23 | syl2anc | |
25 | 1 3 | latmcl | |
26 | 20 24 8 25 | syl3anc | |
27 | 1 4 | opcon3b | |
28 | 7 26 11 27 | syl3anc | |
29 | 1 14 | latjcom | |
30 | 20 22 10 29 | syl3anc | |
31 | omlol | |
|
32 | 31 | 3ad2ant1 | |
33 | 1 14 3 4 | oldmm2 | |
34 | 32 22 8 33 | syl3anc | |
35 | 1 4 | opococ | |
36 | 7 8 35 | syl2anc | |
37 | 36 | oveq2d | |
38 | 37 | oveq2d | |
39 | 30 34 38 | 3eqtr4d | |
40 | 39 | eqeq2d | |
41 | 28 40 | bitrd | |
42 | 16 18 41 | 3imtr4d | |