Metamath Proof Explorer

Theorem atlen0

Description: A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses atlen0.b ⊢ B = Base K
atlen0.l ⊢ ≤ ˙ = ≤ K
atlen0.z ⊢ 0 ˙ = 0. ⁡ K
atlen0.a ⊢ A = Atoms ⁡ K
Assertion atlen0 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → X ≠ 0 ˙

Proof

Step Hyp Ref Expression
1 atlen0.b ⊢ B = Base K
2 atlen0.l ⊢ ≤ ˙ = ≤ K
3 atlen0.z ⊢ 0 ˙ = 0. ⁡ K
4 atlen0.a ⊢ A = Atoms ⁡ K
5 simpl1 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → K ∈ AtLat
6 1 3 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ B
7 5 6 syl ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ ∈ B
8 simpl2 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → X ∈ B
9 5 7 8 3jca ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → K ∈ AtLat ∧ 0 ˙ ∈ B ∧ X ∈ B
10 simpl3 ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → P ∈ A
11 1 4 atbase ⊢ P ∈ A → P ∈ B
12 10 11 syl ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → P ∈ B
13 eqid ⊢ ⋖ K = ⋖ K
14 3 13 4 atcvr0 ⊢ K ∈ AtLat ∧ P ∈ A → 0 ˙ ⋖ K P
15 5 10 14 syl2anc ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ ⋖ K P
16 eqid ⊢ < K = < K
17 1 16 13 cvrlt ⊢ K ∈ AtLat ∧ 0 ˙ ∈ B ∧ P ∈ B ∧ 0 ˙ ⋖ K P → 0 ˙ < K P
18 5 7 12 15 17 syl31anc ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ < K P
19 simpr ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → P ≤ ˙ X
20 atlpos ⊢ K ∈ AtLat → K ∈ Poset
21 5 20 syl ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → K ∈ Poset
22 1 2 16 pltletr ⊢ K ∈ Poset ∧ 0 ˙ ∈ B ∧ P ∈ B ∧ X ∈ B → 0 ˙ < K P ∧ P ≤ ˙ X → 0 ˙ < K X
23 21 7 12 8 22 syl13anc ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ < K P ∧ P ≤ ˙ X → 0 ˙ < K X
24 18 19 23 mp2and ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ < K X
25 16 pltne ⊢ K ∈ AtLat ∧ 0 ˙ ∈ B ∧ X ∈ B → 0 ˙ < K X → 0 ˙ ≠ X
26 9 24 25 sylc ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → 0 ˙ ≠ X
27 26 necomd ⊢ K ∈ AtLat ∧ X ∈ B ∧ P ∈ A ∧ P ≤ ˙ X → X ≠ 0 ˙