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