Metamath Proof Explorer


Theorem oldmm2

Description: De Morgan's law for meet in an ortholattice. ( chdmm2 analog.) (Contributed by NM, 6-Nov-2011)

Ref Expression
Hypotheses oldmm1.b B=BaseK
oldmm1.j ˙=joinK
oldmm1.m ˙=meetK
oldmm1.o ˙=ocK
Assertion oldmm2 KOLXBYB˙˙X˙Y=X˙˙Y

Proof

Step Hyp Ref Expression
1 oldmm1.b B=BaseK
2 oldmm1.j ˙=joinK
3 oldmm1.m ˙=meetK
4 oldmm1.o ˙=ocK
5 olop KOLKOP
6 1 4 opoccl KOPXB˙XB
7 5 6 sylan KOLXB˙XB
8 7 3adant3 KOLXBYB˙XB
9 1 2 3 4 oldmm1 KOL˙XBYB˙˙X˙Y=˙˙X˙˙Y
10 8 9 syld3an2 KOLXBYB˙˙X˙Y=˙˙X˙˙Y
11 1 4 opococ KOPXB˙˙X=X
12 5 11 sylan KOLXB˙˙X=X
13 12 3adant3 KOLXBYB˙˙X=X
14 13 oveq1d KOLXBYB˙˙X˙˙Y=X˙˙Y
15 10 14 eqtrd KOLXBYB˙˙X˙Y=X˙˙Y