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

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