Theorem olj02

Description: An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012)

	Ref	Expression
Hypotheses	olj0.b	$$⊢B={\mathrm{Base}}_K$$
	olj0.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	olj0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	olj02	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\vee }X=X$$

Proof

Step	Hyp	Ref	Expression
1		olj0.b	$$⊢B={\mathrm{Base}}_K$$
2		olj0.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		olj0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		ollat	$$⊢K\in \mathrm{OL}\to K\in \mathrm{Lat}$$
5	4	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to K\in \mathrm{Lat}$$
6		olop	$$⊢K\in \mathrm{OL}\to K\in \mathrm{OP}$$
7	1 3	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in B$$
8	6 7	syl	$$⊢K\in \mathrm{OL}\to \underset{\dot{}}{0}\in B$$
9	8	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\in B$$
10		simpr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\in B$$
11	1 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge \underset{\dot{}}{0}\in B\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }\underset{\dot{}}{0}$$
12	5 9 10 11	syl3anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }\underset{\dot{}}{0}$$
13	1 2 3	olj01	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\vee }\underset{\dot{}}{0}=X$$
14	12 13	eqtrd	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\vee }X=X$$