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

Metamath Proof Explorer

Theorem lhpn0

Description: A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013)

Ref Expression
Hypotheses lhpne0.z 
|- .0. = ( 0. ` K )
lhpne0.h 
|- H = ( LHyp ` K )
Assertion lhpn0 
|- ( ( K e. HL /\ W e. H ) -> W =/= .0. )

Proof

Step Hyp Ref Expression
1 lhpne0.z 
 |-  .0. = ( 0. ` K )
2 lhpne0.h 
 |-  H = ( LHyp ` K )
3 eqid 
 |-  ( lt ` K ) = ( lt ` K )
4 3 1 2 lhp0lt 
 |-  ( ( K e. HL /\ W e. H ) -> .0. ( lt ` K ) W )
5 simpl 
 |-  ( ( K e. HL /\ W e. H ) -> K e. HL )
6 hlop 
 |-  ( K e. HL -> K e. OP )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 1 op0cl 
 |-  ( K e. OP -> .0. e. ( Base ` K ) )
9 6 8 syl 
 |-  ( K e. HL -> .0. e. ( Base ` K ) )
10 9 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> .0. e. ( Base ` K ) )
11 simpr 
 |-  ( ( K e. HL /\ W e. H ) -> W e. H )
12 3 pltne 
 |-  ( ( K e. HL /\ .0. e. ( Base ` K ) /\ W e. H ) -> ( .0. ( lt ` K ) W -> .0. =/= W ) )
13 5 10 11 12 syl3anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( .0. ( lt ` K ) W -> .0. =/= W ) )
14 4 13 mpd 
 |-  ( ( K e. HL /\ W e. H ) -> .0. =/= W )
15 14 necomd 
 |-  ( ( K e. HL /\ W e. H ) -> W =/= .0. )