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

Metamath Proof Explorer

Theorem 2llnneN

Description: Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2lnne.l ⊢ ≤ ˙ = ≤ K
2 2lnne.j ⊢ ∨ ˙ = join ⁡ K
3 2lnne.a ⊢ A = Atoms ⁡ K
4 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → K ∈ HL
5 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ A
6 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∈ A
7 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → P ∈ A
8 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → R ∈ A
9 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → Q ∈ A
10 7 8 9 3jca ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → P ∈ A ∧ R ∈ A ∧ Q ∈ A
11 1 2 3 hlatexch2 ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A ∧ Q ∈ A ∧ P ≠ Q → P ≤ ˙ R ∨ ˙ Q → R ≤ ˙ P ∨ ˙ Q
12 10 11 syld3an2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → P ≤ ˙ R ∨ ˙ Q → R ≤ ˙ P ∨ ˙ Q
13 12 con3d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q → ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ R ∨ ˙ Q
14 13 3exp ⊢ K ∈ HL → P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ≠ Q → ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ R ∨ ˙ Q
15 14 imp4a ⊢ K ∈ HL → P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ R ∨ ˙ Q
16 15 3imp ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ P ≤ ˙ R ∨ ˙ Q
17 1 2 3 2llnne2N ⊢ K ∈ HL ∧ P ∈ A ∧ R ∈ A ∧ ¬ P ≤ ˙ R ∨ ˙ Q → R ∨ ˙ P ≠ R ∨ ˙ Q
18 4 5 6 16 17 syl121anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ≠ Q ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∨ ˙ P ≠ R ∨ ˙ Q