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

Metamath Proof Explorer

Theorem olj02

Description: An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012)

Ref Expression
Hypotheses olj0.b ⊢ B = Base K
olj0.j ⊢ ∨ ˙ = join ⁡ K
olj0.z ⊢ 0 ˙ = 0. ⁡ K
Assertion olj02 ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ∨ ˙ X = X

Proof

Step Hyp Ref Expression
1 olj0.b ⊢ B = Base K
2 olj0.j ⊢ ∨ ˙ = join ⁡ K
3 olj0.z ⊢ 0 ˙ = 0. ⁡ K
4 ollat ⊢ K ∈ OL → K ∈ Lat
5 4 adantr ⊢ K ∈ OL ∧ X ∈ B → K ∈ Lat
6 olop ⊢ K ∈ OL → K ∈ OP
7 1 3 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
8 6 7 syl ⊢ K ∈ OL → 0 ˙ ∈ B
9 8 adantr ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ∈ B
10 simpr ⊢ K ∈ OL ∧ X ∈ B → X ∈ B
11 1 2 latjcom ⊢ K ∈ Lat ∧ 0 ˙ ∈ B ∧ X ∈ B → 0 ˙ ∨ ˙ X = X ∨ ˙ 0 ˙
12 5 9 10 11 syl3anc ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ∨ ˙ X = X ∨ ˙ 0 ˙
13 1 2 3 olj01 ⊢ K ∈ OL ∧ X ∈ B → X ∨ ˙ 0 ˙ = X
14 12 13 eqtrd ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ∨ ˙ X = X