Metamath Proof Explorer

Theorem lhpm0atN

Description: If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lhpm0at.b 
|- B = ( Base ` K )
lhpm0at.m 
|- ./\ = ( meet ` K )
lhpm0at.o 
|- .0. = ( 0. ` K )
lhpm0at.a 
|- A = ( Atoms ` K )
lhpm0at.h 
|- H = ( LHyp ` K )
Assertion lhpm0atN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> X e. A )

Proof

Step Hyp Ref Expression
1 lhpm0at.b 
 |-  B = ( Base ` K )
2 lhpm0at.m 
 |-  ./\ = ( meet ` K )
3 lhpm0at.o 
 |-  .0. = ( 0. ` K )
4 lhpm0at.a 
 |-  A = ( Atoms ` K )
5 lhpm0at.h 
 |-  H = ( LHyp ` K )
6 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X ./\ W ) = .0. )
7 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( K e. HL /\ W e. H ) )
8 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> X e. B )
9 simpr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> X =/= .0. )
10 hllat 
 |-  ( K e. HL -> K e. Lat )
11 10 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> K e. Lat )
12 1 5 lhpbase 
 |-  ( W e. H -> W e. B )
13 12 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> W e. B )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 1 14 2 latleeqm1 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ( le ` K ) W <-> ( X ./\ W ) = X ) )
16 11 8 13 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X ( le ` K ) W <-> ( X ./\ W ) = X ) )
17 16 biimpa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) /\ X ( le ` K ) W ) -> ( X ./\ W ) = X )
18 simplr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) /\ X ( le ` K ) W ) -> ( X ./\ W ) = .0. )
19 17 18 eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) /\ X ( le ` K ) W ) -> X = .0. )
20 19 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X ( le ` K ) W -> X = .0. ) )
21 20 necon3ad 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X =/= .0. -> -. X ( le ` K ) W ) )
22 9 21 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> -. X ( le ` K ) W )
23 eqid 
 |-  (
24 1 14 2 23 5 lhpmcvr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X ( le ` K ) W ) ) -> ( X ./\ W ) (
25 7 8 22 24 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X ./\ W ) (
26 6 25 eqbrtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> .0. (
27 simpll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> K e. HL )
28 1 3 23 4 isat2 
 |-  ( ( K e. HL /\ X e. B ) -> ( X e. A <-> .0. (
29 27 8 28 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> ( X e. A <-> .0. (
30 26 29 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> X e. A )