Theorem olm12

Description: The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012)

	Ref	Expression
Hypotheses	olm1.b	$$⊢B={\mathrm{Base}}_K$$
	olm1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	olm1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	olm12	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\wedge }X=X$$

Proof

Step	Hyp	Ref	Expression
1		olm1.b	$$⊢B={\mathrm{Base}}_K$$
2		olm1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		olm1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\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	6	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to K\in \mathrm{OP}$$
8	1 3	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in B$$
9	7 8	syl	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{1}\in B$$
10		simpr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\in B$$
11	1 2	latmcom	$$⊢\left(K\in \mathrm{Lat}\wedge \underset{\dot{}}{1}\in B\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\wedge }X=X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}$$
12	5 9 10 11	syl3anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\wedge }X=X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}$$
13	1 2 3	olm11	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{1}=X$$
14	12 13	eqtrd	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\wedge }X=X$$