Metamath Proof Explorer

Theorem 2atnelpln

Description: The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012)

Ref Expression
Hypotheses 2atnelpln.j ⊢ ∨ ˙ = join ⁡ K
2atnelpln.a ⊢ A = Atoms ⁡ K
2atnelpln.p ⊢ P = LPlanes ⁡ K
Assertion 2atnelpln ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → ¬ Q ∨ ˙ R ∈ P

Proof

Step Hyp Ref Expression
1 2atnelpln.j ⊢ ∨ ˙ = join ⁡ K
2 2atnelpln.a ⊢ A = Atoms ⁡ K
3 2atnelpln.p ⊢ P = LPlanes ⁡ K
4 hllat ⊢ K ∈ HL → K ∈ Lat
5 4 3ad2ant1 ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → K ∈ Lat
6 eqid ⊢ Base K = Base K
7 6 1 2 hlatjcl ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R ∈ Base K
8 eqid ⊢ ≤ K = ≤ K
9 6 8 latref ⊢ K ∈ Lat ∧ Q ∨ ˙ R ∈ Base K → Q ∨ ˙ R ≤ K Q ∨ ˙ R
10 5 7 9 syl2anc ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R ≤ K Q ∨ ˙ R
11 simpl1 ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ Q ∨ ˙ R ∈ P → K ∈ HL
12 simpr ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ Q ∨ ˙ R ∈ P → Q ∨ ˙ R ∈ P
13 simpl2 ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ Q ∨ ˙ R ∈ P → Q ∈ A
14 simpl3 ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ Q ∨ ˙ R ∈ P → R ∈ A
15 8 1 2 3 lplnnle2at ⊢ K ∈ HL ∧ Q ∨ ˙ R ∈ P ∧ Q ∈ A ∧ R ∈ A → ¬ Q ∨ ˙ R ≤ K Q ∨ ˙ R
16 11 12 13 14 15 syl13anc ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A ∧ Q ∨ ˙ R ∈ P → ¬ Q ∨ ˙ R ≤ K Q ∨ ˙ R
17 16 ex ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R ∈ P → ¬ Q ∨ ˙ R ≤ K Q ∨ ˙ R
18 10 17 mt2d ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → ¬ Q ∨ ˙ R ∈ P