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

Metamath Proof Explorer

Theorem lvolbase

Description: A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses lvolbase.b ⊢ B = Base K
lvolbase.v ⊢ V = LVols ⁡ K
Assertion lvolbase ⊢ X ∈ V → X ∈ B

Proof

Step Hyp Ref Expression
1 lvolbase.b ⊢ B = Base K
2 lvolbase.v ⊢ V = LVols ⁡ K
3 n0i ⊢ X ∈ V → ¬ V = ∅
4 2 eqeq1i ⊢ V = ∅ ↔ LVols ⁡ K = ∅
5 3 4 sylnib ⊢ X ∈ V → ¬ LVols ⁡ K = ∅
6 fvprc ⊢ ¬ K ∈ V → LVols ⁡ K = ∅
7 5 6 nsyl2 ⊢ X ∈ V → K ∈ V
8 eqid ⊢ ⋖ K = ⋖ K
9 eqid ⊢ LPlanes ⁡ K = LPlanes ⁡ K
10 1 8 9 2 islvol ⊢ K ∈ V → X ∈ V ↔ X ∈ B ∧ ∃ x ∈ LPlanes ⁡ K x ⋖ K X
11 10 simprbda ⊢ K ∈ V ∧ X ∈ V → X ∈ B
12 7 11 mpancom ⊢ X ∈ V → X ∈ B