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

Metamath Proof Explorer

Theorem omllaw5N

Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omllaw5.b ⊢ B = Base K
omllaw5.j ⊢ ∨ ˙ = join ⁡ K
omllaw5.m ⊢ ∧ ˙ = meet ⁡ K
omllaw5.o ⊢ ⊥ ˙ = oc ⁡ K
Assertion omllaw5N ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ ⊥ ˙ ⁡ X ∧ ˙ X ∨ ˙ Y = X ∨ ˙ Y

Proof

Step Hyp Ref Expression
1 omllaw5.b ⊢ B = Base K
2 omllaw5.j ⊢ ∨ ˙ = join ⁡ K
3 omllaw5.m ⊢ ∧ ˙ = meet ⁡ K
4 omllaw5.o ⊢ ⊥ ˙ = oc ⁡ K
5 simp1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OML
6 simp2 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∈ B
7 omllat ⊢ K ∈ OML → K ∈ Lat
8 1 2 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
9 7 8 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
10 5 6 9 3jca ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OML ∧ X ∈ B ∧ X ∨ ˙ Y ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 latlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ≤ K X ∨ ˙ Y
13 7 12 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ≤ K X ∨ ˙ Y
14 1 11 2 3 4 omllaw2N ⊢ K ∈ OML ∧ X ∈ B ∧ X ∨ ˙ Y ∈ B → X ≤ K X ∨ ˙ Y → X ∨ ˙ ⊥ ˙ ⁡ X ∧ ˙ X ∨ ˙ Y = X ∨ ˙ Y
15 10 13 14 sylc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ ⊥ ˙ ⁡ X ∧ ˙ X ∨ ˙ Y = X ∨ ˙ Y