Metamath Proof Explorer


Theorem oldmj2

Description: De Morgan's law for join in an ortholattice. ( chdmj2 analog.) (Contributed by NM, 7-Nov-2011)

Ref Expression
Hypotheses oldmm1.b B = Base K
oldmm1.j ˙ = join K
oldmm1.m ˙ = meet K
oldmm1.o ˙ = oc K
Assertion oldmj2 K OL X B Y B ˙ ˙ X ˙ Y = X ˙ ˙ Y

Proof

Step Hyp Ref Expression
1 oldmm1.b B = Base K
2 oldmm1.j ˙ = join K
3 oldmm1.m ˙ = meet K
4 oldmm1.o ˙ = oc K
5 olop K OL K OP
6 1 4 opoccl K OP X B ˙ X B
7 5 6 sylan K OL X B ˙ X B
8 7 3adant3 K OL X B Y B ˙ X B
9 1 2 3 4 oldmj1 K OL ˙ X B Y B ˙ ˙ X ˙ Y = ˙ ˙ X ˙ ˙ Y
10 8 9 syld3an2 K OL X B Y B ˙ ˙ X ˙ Y = ˙ ˙ X ˙ ˙ Y
11 1 4 opococ K OP X B ˙ ˙ X = X
12 5 11 sylan K OL X B ˙ ˙ X = X
13 12 3adant3 K OL X B Y B ˙ ˙ X = X
14 13 oveq1d K OL X B Y B ˙ ˙ X ˙ ˙ Y = X ˙ ˙ Y
15 10 14 eqtrd K OL X B Y B ˙ ˙ X ˙ Y = X ˙ ˙ Y