Theorem olm02

Description: Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012)

	Ref	Expression
Hypotheses	olm0.b	$$⊢B={\mathrm{Base}}_K$$
	olm0.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	olm0.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	olm02	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\wedge }X=\underset{\dot{}}{0}$$

Proof

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