Step |
Hyp |
Ref |
Expression |
1 |
|
lplnn0.z |
⊢ 0 = ( 0. ‘ 𝐾 ) |
2 |
|
lplnn0.p |
⊢ 𝑃 = ( LPlanes ‘ 𝐾 ) |
3 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
4 |
3
|
atex |
⊢ ( 𝐾 ∈ HL → ( Atoms ‘ 𝐾 ) ≠ ∅ ) |
5 |
|
n0 |
⊢ ( ( Atoms ‘ 𝐾 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) |
6 |
4 5
|
sylib |
⊢ ( 𝐾 ∈ HL → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) |
8 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
9 |
8 3 2
|
lplnnleat |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 ) |
10 |
9
|
3expa |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 ) |
11 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
12 |
11
|
ad2antrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
14 |
13 3
|
atbase |
⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
15 |
14
|
adantl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
16 |
13 8 1
|
op0le |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 ) |
17 |
12 15 16
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 ) |
18 |
|
breq1 |
⊢ ( 𝑋 = 0 → ( 𝑋 ( le ‘ 𝐾 ) 𝑝 ↔ 0 ( le ‘ 𝐾 ) 𝑝 ) ) |
19 |
17 18
|
syl5ibrcom |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 = 0 → 𝑋 ( le ‘ 𝐾 ) 𝑝 ) ) |
20 |
19
|
necon3bd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 → 𝑋 ≠ 0 ) ) |
21 |
10 20
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ≠ 0 ) |
22 |
7 21
|
exlimddv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ 0 ) |