Theorem olm01

Description: Meet with lattice zero is zero. ( chm0 analog.) (Contributed by NM, 8-Nov-2011)

	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	olm01	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}=\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		eqid	$$⊢{\le }_K={\le }_K$$
5		ollat	$$⊢K\in \mathrm{OL}\to K\in \mathrm{Lat}$$
6	5	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to K\in \mathrm{Lat}$$
7		simpr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\in B$$
8		olop	$$⊢K\in \mathrm{OL}\to K\in \mathrm{OP}$$
9	8	adantr	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to K\in \mathrm{OP}$$
10	1 3	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in B$$
11	9 10	syl	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}\in B$$
12	1 2	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge \underset{\dot{}}{0}\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\in B$$
13	6 7 11 12	syl3anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\in B$$
14	1 4 2	latmle2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge \underset{\dot{}}{0}\in B\right)\to \left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{0}$$
15	6 7 11 14	syl3anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\right){\le }_K\underset{\dot{}}{0}$$
16	1 4 3	op0le	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_{K}X$$
17	8 16	sylan	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_{K}X$$
18	1 4	latref	$$⊢\left(K\in \mathrm{Lat}\wedge \underset{\dot{}}{0}\in B\right)\to \underset{\dot{}}{0}{\le }_K\underset{\dot{}}{0}$$
19	6 11 18	syl2anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_K\underset{\dot{}}{0}$$
20	1 4 2	latlem12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\underset{\dot{}}{0}\in B\wedge X\in B\wedge \underset{\dot{}}{0}\in B\right)\right)\to \left(\left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}{\le }_K\underset{\dot{}}{0}\right)\leftrightarrow \underset{\dot{}}{0}{\le }_K\left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\right)\right)$$
21	6 11 7 11 20	syl13anc	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{0}{\le }_{K}X\wedge \underset{\dot{}}{0}{\le }_K\underset{\dot{}}{0}\right)\leftrightarrow \underset{\dot{}}{0}{\le }_K\left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\right)\right)$$
22	17 19 21	mpbi2and	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to \underset{\dot{}}{0}{\le }_K\left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}\right)$$
23	1 4 6 13 11 15 22	latasymd	$$⊢\left(K\in \mathrm{OL}\wedge X\in B\right)\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{0}=\underset{\dot{}}{0}$$