Metamath Proof Explorer


Theorem oldmj3

Description: De Morgan's law for join in an ortholattice. ( chdmj3 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 oldmj3 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 5 3ad2ant1 K OL X B Y B K OP
7 simp3 K OL X B Y B Y B
8 1 4 opoccl K OP Y B ˙ Y B
9 6 7 8 syl2anc K OL X B Y B ˙ Y B
10 1 2 3 4 oldmj1 K OL X B ˙ Y B ˙ X ˙ ˙ Y = ˙ X ˙ ˙ ˙ Y
11 9 10 syld3an3 K OL X B Y B ˙ X ˙ ˙ Y = ˙ X ˙ ˙ ˙ Y
12 1 4 opococ K OP Y B ˙ ˙ Y = Y
13 6 7 12 syl2anc K OL X B Y B ˙ ˙ Y = Y
14 13 oveq2d K OL X B Y B ˙ X ˙ ˙ ˙ Y = ˙ X ˙ Y
15 11 14 eqtrd K OL X B Y B ˙ X ˙ ˙ Y = ˙ X ˙ Y