This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2llnma2

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012)

Ref Expression
Hypotheses 2llnm.l ⊢ ≤ ˙ = ≤ K
2llnm.j ⊢ ∨ ˙ = join ⁡ K
2llnm.m ⊢ ∧ ˙ = meet ⁡ K
2llnm.a ⊢ A = Atoms ⁡ K
Assertion 2llnma2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∨ ˙ P ∧ ˙ R ∨ ˙ Q = R

Proof

Step Hyp Ref Expression
1 2llnm.l ⊢ ≤ ˙ = ≤ K
2 2llnm.j ⊢ ∨ ˙ = join ⁡ K
3 2llnm.m ⊢ ∧ ˙ = meet ⁡ K
4 2llnm.a ⊢ A = Atoms ⁡ K
5 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → K ∈ HL
6 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ A
7 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∈ A
8 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∈ A
9 1 2 4 4atlem0ae ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ Q ≤ ˙ P ∨ ˙ R
10 1 2 3 4 2llnma1 ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ R → R ∨ ˙ P ∧ ˙ R ∨ ˙ Q = R
11 5 6 7 8 9 10 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∨ ˙ P ∧ ˙ R ∨ ˙ Q = R