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

Metamath Proof Explorer

Theorem 2atnelvolN

Description: The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 3atnelvol.j ⊢ ∨ ˙ = join ⁡ K
3atnelvol.a ⊢ A = Atoms ⁡ K
3atnelvol.v ⊢ V = LVols ⁡ K
Assertion 2atnelvolN ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → ¬ P ∨ ˙ Q ∈ V

Proof

Step Hyp Ref Expression
1 3atnelvol.j ⊢ ∨ ˙ = join ⁡ K
2 3atnelvol.a ⊢ A = Atoms ⁡ K
3 3atnelvol.v ⊢ V = LVols ⁡ K
4 1 2 hlatjidm ⊢ K ∈ HL ∧ P ∈ A → P ∨ ˙ P = P
5 4 3adant3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ P = P
6 5 oveq1d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ P ∨ ˙ Q = P ∨ ˙ Q
7 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → K ∈ HL
8 simp2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∈ A
9 simp3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → Q ∈ A
10 1 2 3 3atnelvolN ⊢ K ∈ HL ∧ P ∈ A ∧ P ∈ A ∧ Q ∈ A → ¬ P ∨ ˙ P ∨ ˙ Q ∈ V
11 7 8 8 9 10 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → ¬ P ∨ ˙ P ∨ ˙ Q ∈ V
12 6 11 eqneltrrd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → ¬ P ∨ ˙ Q ∈ V