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 ∨ 𝑋 ) = 𝑋 )