# Metamath Proof Explorer

## 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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. )`