Theorem olm01

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

	Ref	Expression
Hypotheses	olm0.b	|- B = ( Base ` K )
	olm0.m	|- ./\ = ( meet ` K )
	olm0.z	|- .0. = ( 0. ` K )
Assertion	olm01	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		olm0.b	|- B = ( Base ` K )
2		olm0.m	|- ./\ = ( meet ` K )
3		olm0.z	|- .0. = ( 0. ` K )
4		eqid	|- ( le ` K ) = ( le ` K )
5		ollat	|- ( K e. OL -> K e. Lat )
6	5	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. Lat )
7		simpr	|- ( ( K e. OL /\ X e. B ) -> X e. B )
8		olop	|- ( K e. OL -> K e. OP )
9	8	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. OP )
10	1 3	op0cl	|- ( K e. OP -> .0. e. B )
11	9 10	syl	|- ( ( K e. OL /\ X e. B ) -> .0. e. B )
12	1 2	latmcl	|- ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> ( X ./\ .0. ) e. B )
13	6 7 11 12	syl3anc	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) e. B )
14	1 4 2	latmle2	|- ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> ( X ./\ .0. ) ( le ` K ) .0. )
15	6 7 11 14	syl3anc	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) ( le ` K ) .0. )
16	1 4 3	op0le	|- ( ( K e. OP /\ X e. B ) -> .0. ( le ` K ) X )
17	8 16	sylan	|- ( ( K e. OL /\ X e. B ) -> .0. ( le ` K ) X )
18	1 4	latref	|- ( ( K e. Lat /\ .0. e. B ) -> .0. ( le ` K ) .0. )
19	6 11 18	syl2anc	|- ( ( K e. OL /\ X e. B ) -> .0. ( le ` K ) .0. )
20	1 4 2	latlem12	|- ( ( K e. Lat /\ ( .0. e. B /\ X e. B /\ .0. e. B ) ) -> ( ( .0. ( le ` K ) X /\ .0. ( le ` K ) .0. ) <-> .0. ( le ` K ) ( X ./\ .0. ) ) )
21	6 11 7 11 20	syl13anc	|- ( ( K e. OL /\ X e. B ) -> ( ( .0. ( le ` K ) X /\ .0. ( le ` K ) .0. ) <-> .0. ( le ` K ) ( X ./\ .0. ) ) )
22	17 19 21	mpbi2and	|- ( ( K e. OL /\ X e. B ) -> .0. ( le ` K ) ( X ./\ .0. ) )
23	1 4 6 13 11 15 22	latasymd	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) = .0. )