Metamath Proof Explorer


Theorem lhpocnle

Description: The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses lhpocnle.l
|- .<_ = ( le ` K )
lhpocnle.o
|- ._|_ = ( oc ` K )
lhpocnle.h
|- H = ( LHyp ` K )
Assertion lhpocnle
|- ( ( K e. HL /\ W e. H ) -> -. ( ._|_ ` W ) .<_ W )

Proof

Step Hyp Ref Expression
1 lhpocnle.l
 |-  .<_ = ( le ` K )
2 lhpocnle.o
 |-  ._|_ = ( oc ` K )
3 lhpocnle.h
 |-  H = ( LHyp ` K )
4 hlatl
 |-  ( K e. HL -> K e. AtLat )
5 4 adantr
 |-  ( ( K e. HL /\ W e. H ) -> K e. AtLat )
6 simpr
 |-  ( ( K e. HL /\ W e. H ) -> W e. H )
7 eqid
 |-  ( Base ` K ) = ( Base ` K )
8 7 3 lhpbase
 |-  ( W e. H -> W e. ( Base ` K ) )
9 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 7 2 9 3 lhpoc
 |-  ( ( K e. HL /\ W e. ( Base ` K ) ) -> ( W e. H <-> ( ._|_ ` W ) e. ( Atoms ` K ) ) )
11 8 10 sylan2
 |-  ( ( K e. HL /\ W e. H ) -> ( W e. H <-> ( ._|_ ` W ) e. ( Atoms ` K ) ) )
12 6 11 mpbid
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` W ) e. ( Atoms ` K ) )
13 eqid
 |-  ( 0. ` K ) = ( 0. ` K )
14 13 9 atn0
 |-  ( ( K e. AtLat /\ ( ._|_ ` W ) e. ( Atoms ` K ) ) -> ( ._|_ ` W ) =/= ( 0. ` K ) )
15 5 12 14 syl2anc
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` W ) =/= ( 0. ` K ) )
16 15 neneqd
 |-  ( ( K e. HL /\ W e. H ) -> -. ( ._|_ ` W ) = ( 0. ` K ) )
17 simpr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) .<_ W )
18 hllat
 |-  ( K e. HL -> K e. Lat )
19 18 ad2antrr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> K e. Lat )
20 hlop
 |-  ( K e. HL -> K e. OP )
21 20 ad2antrr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> K e. OP )
22 8 ad2antlr
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> W e. ( Base ` K ) )
23 7 2 opoccl
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ._|_ ` W ) e. ( Base ` K ) )
24 21 22 23 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) e. ( Base ` K ) )
25 7 1 latref
 |-  ( ( K e. Lat /\ ( ._|_ ` W ) e. ( Base ` K ) ) -> ( ._|_ ` W ) .<_ ( ._|_ ` W ) )
26 19 24 25 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) .<_ ( ._|_ ` W ) )
27 eqid
 |-  ( meet ` K ) = ( meet ` K )
28 7 1 27 latlem12
 |-  ( ( K e. Lat /\ ( ( ._|_ ` W ) e. ( Base ` K ) /\ W e. ( Base ` K ) /\ ( ._|_ ` W ) e. ( Base ` K ) ) ) -> ( ( ( ._|_ ` W ) .<_ W /\ ( ._|_ ` W ) .<_ ( ._|_ ` W ) ) <-> ( ._|_ ` W ) .<_ ( W ( meet ` K ) ( ._|_ ` W ) ) ) )
29 19 24 22 24 28 syl13anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ( ( ._|_ ` W ) .<_ W /\ ( ._|_ ` W ) .<_ ( ._|_ ` W ) ) <-> ( ._|_ ` W ) .<_ ( W ( meet ` K ) ( ._|_ ` W ) ) ) )
30 17 26 29 mpbi2and
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) .<_ ( W ( meet ` K ) ( ._|_ ` W ) ) )
31 7 2 27 13 opnoncon
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( W ( meet ` K ) ( ._|_ ` W ) ) = ( 0. ` K ) )
32 21 22 31 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( W ( meet ` K ) ( ._|_ ` W ) ) = ( 0. ` K ) )
33 30 32 breqtrd
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) .<_ ( 0. ` K ) )
34 7 1 13 ople0
 |-  ( ( K e. OP /\ ( ._|_ ` W ) e. ( Base ` K ) ) -> ( ( ._|_ ` W ) .<_ ( 0. ` K ) <-> ( ._|_ ` W ) = ( 0. ` K ) ) )
35 21 24 34 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ( ._|_ ` W ) .<_ ( 0. ` K ) <-> ( ._|_ ` W ) = ( 0. ` K ) ) )
36 33 35 mpbid
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` W ) .<_ W ) -> ( ._|_ ` W ) = ( 0. ` K ) )
37 16 36 mtand
 |-  ( ( K e. HL /\ W e. H ) -> -. ( ._|_ ` W ) .<_ W )