Theorem olm02

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

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

Proof

Step	Hyp	Ref	Expression
1		olm0.b	|- B = ( Base ` K )
2		olm0.m	|- ./\ = ( meet ` K )
3		olm0.z	|- .0. = ( 0. ` K )
4		ollat	|- ( K e. OL -> K e. Lat )
5	4	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. Lat )
6		simpr	|- ( ( K e. OL /\ X e. B ) -> X e. B )
7		olop	|- ( K e. OL -> K e. OP )
8	7	adantr	|- ( ( K e. OL /\ X e. B ) -> K e. OP )
9	1 3	op0cl	|- ( K e. OP -> .0. e. B )
10	8 9	syl	|- ( ( K e. OL /\ X e. B ) -> .0. e. B )
11	1 2	latmcom	|- ( ( K e. Lat /\ X e. B /\ .0. e. B ) -> ( X ./\ .0. ) = ( .0. ./\ X ) )
12	5 6 10 11	syl3anc	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) = ( .0. ./\ X ) )
13	1 2 3	olm01	|- ( ( K e. OL /\ X e. B ) -> ( X ./\ .0. ) = .0. )
14	12 13	eqtr3d	|- ( ( K e. OL /\ X e. B ) -> ( .0. ./\ X ) = .0. )