Metamath Proof Explorer

Theorem oldmm4

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

Ref Expression
Hypotheses oldmm1.b ⊢ B = Base K
oldmm1.j ⊢ ∨ ˙ = join ⁡ K
oldmm1.m ⊢ ∧ ˙ = meet ⁡ K
oldmm1.o ⊢ ⊥ ˙ = oc ⁡ K
Assertion oldmm4 ⊢ 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 ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
7 5 6 sylan ⊢ K ∈ OL ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
8 7 3adant2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
9 1 2 3 4 oldmm2 ⊢ K ∈ OL ∧ X ∈ B ∧ ⊥ ˙ ⁡ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ˙ ⊥ ˙ ⁡ Y = X ∨ ˙ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
10 8 9 syld3an3 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ˙ ⊥ ˙ ⁡ Y = X ∨ ˙ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
11 1 4 opococ ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
12 5 11 sylan ⊢ K ∈ OL ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
13 12 3adant2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
14 13 oveq2d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = X ∨ ˙ Y
15 10 14 eqtrd ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ˙ ⊥ ˙ ⁡ Y = X ∨ ˙ Y