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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
olj0.j ⊢ ∨ = ( join ‘ 𝐾 )
olj0.z ⊢ 0 = ( 0. ‘ 𝐾 )
Assertion olj02 ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∨ 𝑋 ) = 𝑋 )

Proof

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