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 = Base K
omllaw5.j ˙ = join K
omllaw5.m ˙ = meet K
omllaw5.o ˙ = oc K
Assertion omllaw5N K OML X B Y B X ˙ ˙ X ˙ X ˙ Y = X ˙ Y

Proof

Step Hyp Ref Expression
1 omllaw5.b B = Base K
2 omllaw5.j ˙ = join K
3 omllaw5.m ˙ = meet K
4 omllaw5.o ˙ = oc K
5 simp1 K OML X B Y B K OML
6 simp2 K OML X B Y B X B
7 omllat K OML K Lat
8 1 2 latjcl K Lat X B Y B X ˙ Y B
9 7 8 syl3an1 K OML X B Y B X ˙ Y B
10 5 6 9 3jca K OML X B Y B K OML X B X ˙ Y B
11 eqid K = K
12 1 11 2 latlej1 K Lat X B Y B X K X ˙ Y
13 7 12 syl3an1 K OML X B Y B X K X ˙ Y
14 1 11 2 3 4 omllaw2N K OML X B X ˙ Y B X K X ˙ Y X ˙ ˙ X ˙ X ˙ Y = X ˙ Y
15 10 13 14 sylc K OML X B Y B X ˙ ˙ X ˙ X ˙ Y = X ˙ Y