Metamath Proof Explorer


Theorem omllaw5N

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 B=BaseK
omllaw5.j ˙=joinK
omllaw5.m ˙=meetK
omllaw5.o ˙=ocK
Assertion omllaw5N KOMLXBYBX˙˙X˙X˙Y=X˙Y

Proof

Step Hyp Ref Expression
1 omllaw5.b B=BaseK
2 omllaw5.j ˙=joinK
3 omllaw5.m ˙=meetK
4 omllaw5.o ˙=ocK
5 simp1 KOMLXBYBKOML
6 simp2 KOMLXBYBXB
7 omllat KOMLKLat
8 1 2 latjcl KLatXBYBX˙YB
9 7 8 syl3an1 KOMLXBYBX˙YB
10 5 6 9 3jca KOMLXBYBKOMLXBX˙YB
11 eqid K=K
12 1 11 2 latlej1 KLatXBYBXKX˙Y
13 7 12 syl3an1 KOMLXBYBXKX˙Y
14 1 11 2 3 4 omllaw2N KOMLXBX˙YBXKX˙YX˙˙X˙X˙Y=X˙Y
15 10 13 14 sylc KOMLXBYBX˙˙X˙X˙Y=X˙Y