This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )