Metamath Proof Explorer

Theorem atle

Description: Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses atle.b ⊢ B = Base K
atle.l ⊢ ≤ ˙ = ≤ K
atle.z ⊢ 0 ˙ = 0. ⁡ K
atle.a ⊢ A = Atoms ⁡ K
Assertion atle ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → ∃ p ∈ A p ≤ ˙ X

Proof

Step Hyp Ref Expression
1 atle.b ⊢ B = Base K
2 atle.l ⊢ ≤ ˙ = ≤ K
3 atle.z ⊢ 0 ˙ = 0. ⁡ K
4 atle.a ⊢ A = Atoms ⁡ K
5 simp1 ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → K ∈ HL
6 hlop ⊢ K ∈ HL → K ∈ OP
7 6 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → K ∈ OP
8 1 3 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
9 7 8 syl ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → 0 ˙ ∈ B
10 simp2 ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → X ∈ B
11 simp3 ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → X ≠ 0 ˙
12 eqid ⊢ < K = < K
13 1 12 3 opltn0 ⊢ K ∈ OP ∧ X ∈ B → 0 ˙ < K X ↔ X ≠ 0 ˙
14 7 10 13 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → 0 ˙ < K X ↔ X ≠ 0 ˙
15 11 14 mpbird ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → 0 ˙ < K X
16 eqid ⊢ join ⁡ K = join ⁡ K
17 1 2 12 16 4 hlrelat ⊢ K ∈ HL ∧ 0 ˙ ∈ B ∧ X ∈ B ∧ 0 ˙ < K X → ∃ p ∈ A 0 ˙ < K 0 ˙ join ⁡ K p ∧ 0 ˙ join ⁡ K p ≤ ˙ X
18 5 9 10 15 17 syl31anc ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → ∃ p ∈ A 0 ˙ < K 0 ˙ join ⁡ K p ∧ 0 ˙ join ⁡ K p ≤ ˙ X
19 simpl1 ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → K ∈ HL
20 hlol ⊢ K ∈ HL → K ∈ OL
21 19 20 syl ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → K ∈ OL
22 1 4 atbase ⊢ p ∈ A → p ∈ B
23 22 adantl ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → p ∈ B
24 1 16 3 olj02 ⊢ K ∈ OL ∧ p ∈ B → 0 ˙ join ⁡ K p = p
25 21 23 24 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → 0 ˙ join ⁡ K p = p
26 25 breq1d ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → 0 ˙ join ⁡ K p ≤ ˙ X ↔ p ≤ ˙ X
27 26 biimpd ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → 0 ˙ join ⁡ K p ≤ ˙ X → p ≤ ˙ X
28 27 adantld ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ ∧ p ∈ A → 0 ˙ < K 0 ˙ join ⁡ K p ∧ 0 ˙ join ⁡ K p ≤ ˙ X → p ≤ ˙ X
29 28 reximdva ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → ∃ p ∈ A 0 ˙ < K 0 ˙ join ⁡ K p ∧ 0 ˙ join ⁡ K p ≤ ˙ X → ∃ p ∈ A p ≤ ˙ X
30 18 29 mpd ⊢ K ∈ HL ∧ X ∈ B ∧ X ≠ 0 ˙ → ∃ p ∈ A p ≤ ˙ X