Metamath Proof Explorer

Theorem islpln2

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)

Ref Expression
Hypotheses islpln5.b ⊢ B = Base K
islpln5.l ⊢ ≤ ˙ = ≤ K
islpln5.j ⊢ ∨ ˙ = join ⁡ K
islpln5.a ⊢ A = Atoms ⁡ K
islpln5.p ⊢ P = LPlanes ⁡ K
Assertion islpln2 ⊢ K ∈ HL → X ∈ P ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ X = p ∨ ˙ q ∨ ˙ r

Proof

Step Hyp Ref Expression
1 islpln5.b ⊢ B = Base K
2 islpln5.l ⊢ ≤ ˙ = ≤ K
3 islpln5.j ⊢ ∨ ˙ = join ⁡ K
4 islpln5.a ⊢ A = Atoms ⁡ K
5 islpln5.p ⊢ P = LPlanes ⁡ K
6 1 5 lplnbase ⊢ X ∈ P → X ∈ B
7 6 pm4.71ri ⊢ X ∈ P ↔ X ∈ B ∧ X ∈ P
8 1 2 3 4 5 islpln5 ⊢ K ∈ HL ∧ X ∈ B → X ∈ P ↔ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ X = p ∨ ˙ q ∨ ˙ r
9 8 pm5.32da ⊢ K ∈ HL → X ∈ B ∧ X ∈ P ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ X = p ∨ ˙ q ∨ ˙ r
10 7 9 syl5bb ⊢ K ∈ HL → X ∈ P ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ X = p ∨ ˙ q ∨ ˙ r