Metamath Proof Explorer


Theorem isomliN

Description: Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

Ref Expression
Hypotheses isomli.0 KOL
isomli.b B=BaseK
isomli.l ˙=K
isomli.j ˙=joinK
isomli.m ˙=meetK
isomli.o ˙=ocK
isomli.7 xByBx˙yy=x˙y˙˙x
Assertion isomliN KOML

Proof

Step Hyp Ref Expression
1 isomli.0 KOL
2 isomli.b B=BaseK
3 isomli.l ˙=K
4 isomli.j ˙=joinK
5 isomli.m ˙=meetK
6 isomli.o ˙=ocK
7 isomli.7 xByBx˙yy=x˙y˙˙x
8 7 rgen2 xByBx˙yy=x˙y˙˙x
9 2 3 4 5 6 isoml KOMLKOLxByBx˙yy=x˙y˙˙x
10 1 8 9 mpbir2an KOML