Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omllaw5.b | |
|
omllaw5.j | |
||
omllaw5.m | |
||
omllaw5.o | |
||
Assertion | omllaw5N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omllaw5.b | |
|
2 | omllaw5.j | |
|
3 | omllaw5.m | |
|
4 | omllaw5.o | |
|
5 | simp1 | |
|
6 | simp2 | |
|
7 | omllat | |
|
8 | 1 2 | latjcl | |
9 | 7 8 | syl3an1 | |
10 | 5 6 9 | 3jca | |
11 | eqid | |
|
12 | 1 11 2 | latlej1 | |
13 | 7 12 | syl3an1 | |
14 | 1 11 2 3 4 | omllaw2N | |
15 | 10 13 14 | sylc | |