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