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 ∈ HL ∧ W ∈ H → W ≠ 0 ˙

Proof

Step Hyp Ref Expression
1 lhpne0.z ⊢ 0 ˙ = 0. ⁡ K
2 lhpne0.h ⊢ H = LHyp ⁡ K
3 eqid ⊢ < K = < K
4 3 1 2 lhp0lt ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ < K W
5 simpl ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL
6 hlop ⊢ K ∈ HL → K ∈ OP
7 eqid ⊢ Base K = Base K
8 7 1 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
9 6 8 syl ⊢ K ∈ HL → 0 ˙ ∈ Base K
10 9 adantr ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base K
11 simpr ⊢ K ∈ HL ∧ W ∈ H → W ∈ H
12 3 pltne ⊢ K ∈ HL ∧ 0 ˙ ∈ Base K ∧ W ∈ H → 0 ˙ < K W → 0 ˙ ≠ W
13 5 10 11 12 syl3anc ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ < K W → 0 ˙ ≠ W
14 4 13 mpd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ≠ W
15 14 necomd ⊢ K ∈ HL ∧ W ∈ H → W ≠ 0 ˙