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

Metamath Proof Explorer

Theorem 2atmat0

Description: The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses 2atmatz.j ⊢ ∨ ˙ = join ⁡ K
2atmatz.m ⊢ ∧ ˙ = meet ⁡ K
2atmatz.z ⊢ 0 ˙ = 0. ⁡ K
2atmatz.a ⊢ A = Atoms ⁡ K
Assertion 2atmat0 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → P ∨ ˙ Q ∧ ˙ R ∨ ˙ S ∈ A ∨ P ∨ ˙ Q ∧ ˙ R ∨ ˙ S = 0 ˙

Proof

Step Hyp Ref Expression
1 2atmatz.j ⊢ ∨ ˙ = join ⁡ K
2 2atmatz.m ⊢ ∧ ˙ = meet ⁡ K
3 2atmatz.z ⊢ 0 ˙ = 0. ⁡ K
4 2atmatz.a ⊢ A = Atoms ⁡ K
5 simpl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → K ∈ HL ∧ P ∈ A ∧ Q ∈ A
6 simpr1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → R ∈ A
7 simpr2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → S ∈ A
8 7 orcd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → S ∈ A ∨ S = 0 ˙
9 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → P ∨ ˙ Q ≠ R ∨ ˙ S
10 1 2 3 4 2at0mat0 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∨ S = 0 ˙ ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → P ∨ ˙ Q ∧ ˙ R ∨ ˙ S ∈ A ∨ P ∨ ˙ Q ∧ ˙ R ∨ ˙ S = 0 ˙
11 5 6 8 9 10 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ P ∨ ˙ Q ≠ R ∨ ˙ S → P ∨ ˙ Q ∧ ˙ R ∨ ˙ S ∈ A ∨ P ∨ ˙ Q ∧ ˙ R ∨ ˙ S = 0 ˙