This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oldmm3N

Description: De Morgan's law for meet in an ortholattice. ( chdmm3 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses oldmm1.b ⊢ B = Base K
oldmm1.j ⊢ ∨ ˙ = join ⁡ K
oldmm1.m ⊢ ∧ ˙ = meet ⁡ K
oldmm1.o ⊢ ⊥ ˙ = oc ⁡ K
Assertion oldmm3N ⊢ 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 oldmm1 ⊢ 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