Metamath Proof Explorer


Theorem omllaw2N

Description: Variation of orthomodular law. Definition of OML law in Kalmbach p. 22. ( pjoml2i analog.) (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omllaw.b B = Base K
omllaw.l ˙ = K
omllaw.j ˙ = join K
omllaw.m ˙ = meet K
omllaw.o ˙ = oc K
Assertion omllaw2N K OML X B Y B X ˙ Y X ˙ ˙ X ˙ Y = Y

Proof

Step Hyp Ref Expression
1 omllaw.b B = Base K
2 omllaw.l ˙ = K
3 omllaw.j ˙ = join K
4 omllaw.m ˙ = meet K
5 omllaw.o ˙ = oc K
6 1 2 3 4 5 omllaw K OML X B Y B X ˙ Y Y = X ˙ Y ˙ ˙ X
7 eqcom X ˙ ˙ X ˙ Y = Y Y = X ˙ ˙ X ˙ Y
8 omllat K OML K Lat
9 8 3ad2ant1 K OML X B Y B K Lat
10 omlop K OML K OP
11 1 5 opoccl K OP X B ˙ X B
12 10 11 sylan K OML X B ˙ X B
13 12 3adant3 K OML X B Y B ˙ X B
14 simp3 K OML X B Y B Y B
15 1 4 latmcom K Lat ˙ X B Y B ˙ X ˙ Y = Y ˙ ˙ X
16 9 13 14 15 syl3anc K OML X B Y B ˙ X ˙ Y = Y ˙ ˙ X
17 16 oveq2d K OML X B Y B X ˙ ˙ X ˙ Y = X ˙ Y ˙ ˙ X
18 17 eqeq2d K OML X B Y B Y = X ˙ ˙ X ˙ Y Y = X ˙ Y ˙ ˙ X
19 7 18 syl5bb K OML X B Y B X ˙ ˙ X ˙ Y = Y Y = X ˙ Y ˙ ˙ X
20 6 19 sylibrd K OML X B Y B X ˙ Y X ˙ ˙ X ˙ Y = Y