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

Metamath Proof Explorer

Theorem islvol2

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses islvol5.b ⊢ B = Base K
islvol5.l ⊢ ≤ ˙ = ≤ K
islvol5.j ⊢ ∨ ˙ = join ⁡ K
islvol5.a ⊢ A = Atoms ⁡ K
islvol5.v ⊢ V = LVols ⁡ K
Assertion islvol2 ⊢ K ∈ HL → X ∈ V ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A ∃ s ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ ¬ s ≤ ˙ p ∨ ˙ q ∨ ˙ r ∧ X = p ∨ ˙ q ∨ ˙ r ∨ ˙ s

Proof

Step Hyp Ref Expression
1 islvol5.b ⊢ B = Base K
2 islvol5.l ⊢ ≤ ˙ = ≤ K
3 islvol5.j ⊢ ∨ ˙ = join ⁡ K
4 islvol5.a ⊢ A = Atoms ⁡ K
5 islvol5.v ⊢ V = LVols ⁡ K
6 1 5 lvolbase ⊢ X ∈ V → X ∈ B
7 6 pm4.71ri ⊢ X ∈ V ↔ X ∈ B ∧ X ∈ V
8 1 2 3 4 5 islvol5 ⊢ K ∈ HL ∧ X ∈ B → X ∈ V ↔ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A ∃ s ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ ¬ s ≤ ˙ p ∨ ˙ q ∨ ˙ r ∧ X = p ∨ ˙ q ∨ ˙ r ∨ ˙ s
9 8 pm5.32da ⊢ K ∈ HL → X ∈ B ∧ X ∈ V ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A ∃ s ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ ¬ s ≤ ˙ p ∨ ˙ q ∨ ˙ r ∧ X = p ∨ ˙ q ∨ ˙ r ∨ ˙ s
10 7 9 bitrid ⊢ K ∈ HL → X ∈ V ↔ X ∈ B ∧ ∃ p ∈ A ∃ q ∈ A ∃ r ∈ A ∃ s ∈ A p ≠ q ∧ ¬ r ≤ ˙ p ∨ ˙ q ∧ ¬ s ≤ ˙ p ∨ ˙ q ∨ ˙ r ∧ X = p ∨ ˙ q ∨ ˙ r ∨ ˙ s