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. ‘ 𝐾 )
	lhpne0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpn0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		lhpne0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		lhpne0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
4	3 1 2	lhp0lt	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ( lt ‘ 𝐾 ) 𝑊 )
5		simpl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ HL )
6		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 1	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
9	6 8	syl	⊢ ( 𝐾 ∈ HL → 0 ∈ ( Base ‘ 𝐾 ) )
10	9	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
11		simpr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ 𝐻 )
12	3	pltne	⊢ ( ( 𝐾 ∈ HL ∧ 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ 𝐻 ) → ( 0 ( lt ‘ 𝐾 ) 𝑊 → 0 ≠ 𝑊 ) )
13	5 10 11 12	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0 ( lt ‘ 𝐾 ) 𝑊 → 0 ≠ 𝑊 ) )
14	4 13	mpd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ≠ 𝑊 )
15	14	necomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ≠ 0 )