Metamath Proof Explorer

Theorem olj01

Description: An ortholattice element joined with zero equals itself. ( chj0 analog.) (Contributed by NM, 19-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 olj0.b ⊢ B = Base K
2 olj0.j ⊢ ∨ ˙ = join ⁡ K
3 olj0.z ⊢ 0 ˙ = 0. ⁡ K
4 olop ⊢ K ∈ OL → K ∈ OP
5 1 3 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
6 4 5 syl ⊢ K ∈ OL → 0 ˙ ∈ B
7 6 adantr ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ∈ B
8 eqid ⊢ ≤ K = ≤ K
9 ollat ⊢ K ∈ OL → K ∈ Lat
10 9 3ad2ant1 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → K ∈ Lat
11 1 2 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ 0 ˙ ∈ B → X ∨ ˙ 0 ˙ ∈ B
12 9 11 syl3an1 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ∨ ˙ 0 ˙ ∈ B
13 simp2 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ∈ B
14 1 8 latref ⊢ K ∈ Lat ∧ X ∈ B → X ≤ K X
15 9 14 sylan ⊢ K ∈ OL ∧ X ∈ B → X ≤ K X
16 15 3adant3 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ≤ K X
17 1 8 3 op0le ⊢ K ∈ OP ∧ X ∈ B → 0 ˙ ≤ K X
18 4 17 sylan ⊢ K ∈ OL ∧ X ∈ B → 0 ˙ ≤ K X
19 18 3adant3 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → 0 ˙ ≤ K X
20 simp3 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → 0 ˙ ∈ B
21 1 8 2 latjle12 ⊢ K ∈ Lat ∧ X ∈ B ∧ 0 ˙ ∈ B ∧ X ∈ B → X ≤ K X ∧ 0 ˙ ≤ K X ↔ X ∨ ˙ 0 ˙ ≤ K X
22 10 13 20 13 21 syl13anc ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ≤ K X ∧ 0 ˙ ≤ K X ↔ X ∨ ˙ 0 ˙ ≤ K X
23 16 19 22 mpbi2and ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ∨ ˙ 0 ˙ ≤ K X
24 1 8 2 latlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ 0 ˙ ∈ B → X ≤ K X ∨ ˙ 0 ˙
25 9 24 syl3an1 ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ≤ K X ∨ ˙ 0 ˙
26 1 8 10 12 13 23 25 latasymd ⊢ K ∈ OL ∧ X ∈ B ∧ 0 ˙ ∈ B → X ∨ ˙ 0 ˙ = X
27 7 26 mpd3an3 ⊢ K ∈ OL ∧ X ∈ B → X ∨ ˙ 0 ˙ = X