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 e. OL /\ X e. 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 e. OL -> K e. Lat )
5	4	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. Lat )
6		olop	|- ( K e. OL -> K e. OP )
7	1 3	op0cl	|- ( K e. OP -> .0. e. B )
8	6 7	syl	|- ( K e. OL -> .0. e. B )
9	8	adantr	|- ( ( K e. OL /\ X e. B ) -> .0. e. B )
10		simpr	|- ( ( K e. OL /\ X e. B ) -> X e. B )
11	1 2	latjcom	|- ( ( K e. Lat /\ .0. e. B /\ X e. B ) -> ( .0. .\/ X ) = ( X .\/ .0. ) )
12	5 9 10 11	syl3anc	|- ( ( K e. OL /\ X e. B ) -> ( .0. .\/ X ) = ( X .\/ .0. ) )
13	1 2 3	olj01	|- ( ( K e. OL /\ X e. B ) -> ( X .\/ .0. ) = X )
14	12 13	eqtrd	|- ( ( K e. OL /\ X e. B ) -> ( .0. .\/ X ) = X )