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