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 )