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

Metamath Proof Explorer

Theorem 2llnma2rN

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnm.l ⊢ ≤ ˙ = ≤ K
2llnm.j ⊢ ∨ ˙ = join ⁡ K
2llnm.m ⊢ ∧ ˙ = meet ⁡ K
2llnm.a ⊢ A = Atoms ⁡ K
Assertion 2llnma2rN ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∨ ˙ R ∧ ˙ Q ∨ ˙ R = 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 2 4 hlatjcom ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A → P ∨ ˙ R = R ∨ ˙ P
9 5 6 7 8 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∨ ˙ R = R ∨ ˙ P
10 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∈ A
11 2 4 hlatjcom ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R = R ∨ ˙ Q
12 5 10 7 11 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∨ ˙ R = R ∨ ˙ Q
13 9 12 oveq12d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∨ ˙ R ∧ ˙ Q ∨ ˙ R = R ∨ ˙ P ∧ ˙ R ∨ ˙ Q
14 1 2 3 4 2llnma2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∨ ˙ P ∧ ˙ R ∨ ˙ Q = R
15 13 14 eqtrd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∨ ˙ R ∧ ˙ Q ∨ ˙ R = R