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

Metamath Proof Explorer

Theorem meetat

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012)

Ref Expression
Hypotheses m.b 
|- B = ( Base ` K )
m.m 
|- ./\ = ( meet ` K )
m.z 
|- .0. = ( 0. ` K )
m.a 
|- A = ( Atoms ` K )
Assertion meetat 
|- ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) )

Proof

Step Hyp Ref Expression
1 m.b 
 |-  B = ( Base ` K )
2 m.m 
 |-  ./\ = ( meet ` K )
3 m.z 
 |-  .0. = ( 0. ` K )
4 m.a 
 |-  A = ( Atoms ` K )
5 ollat 
 |-  ( K e. OL -> K e. Lat )
6 5 3ad2ant1 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> K e. Lat )
7 simp2 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> X e. B )
8 simp3 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> P e. A )
9 1 4 atbase 
 |-  ( P e. A -> P e. B )
10 8 9 syl 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> P e. B )
11 eqid 
 |-  ( le ` K ) = ( le ` K )
12 1 11 2 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X ./\ P ) ( le ` K ) P )
13 6 7 10 12 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( X ./\ P ) ( le ` K ) P )
14 olop 
 |-  ( K e. OL -> K e. OP )
15 14 3ad2ant1 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> K e. OP )
16 1 2 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X ./\ P ) e. B )
17 6 7 10 16 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( X ./\ P ) e. B )
18 1 11 3 4 leatb 
 |-  ( ( K e. OP /\ ( X ./\ P ) e. B /\ P e. A ) -> ( ( X ./\ P ) ( le ` K ) P <-> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) ) )
19 15 17 8 18 syl3anc 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) ( le ` K ) P <-> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) ) )
20 13 19 mpbid 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) )