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. )