Metamath Proof Explorer

Theorem lvoli

Description: Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses lvolset.b ⊢ B = Base K
lvolset.c ⊢ C = ⋖ K
lvolset.p ⊢ P = LPlanes ⁡ K
lvolset.v ⊢ V = LVols ⁡ K
Assertion lvoli ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → Y ∈ V

Proof

Step Hyp Ref Expression
1 lvolset.b ⊢ B = Base K
2 lvolset.c ⊢ C = ⋖ K
3 lvolset.p ⊢ P = LPlanes ⁡ K
4 lvolset.v ⊢ V = LVols ⁡ K
5 simpl2 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → Y ∈ B
6 breq1 ⊢ x = X → x C Y ↔ X C Y
7 6 rspcev ⊢ X ∈ P ∧ X C Y → ∃ x ∈ P x C Y
8 7 3ad2antl3 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → ∃ x ∈ P x C Y
9 simpl1 ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → K ∈ D
10 1 2 3 4 islvol ⊢ K ∈ D → Y ∈ V ↔ Y ∈ B ∧ ∃ x ∈ P x C Y
11 9 10 syl ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → Y ∈ V ↔ Y ∈ B ∧ ∃ x ∈ P x C Y
12 5 8 11 mpbir2and ⊢ K ∈ D ∧ Y ∈ B ∧ X ∈ P ∧ X C Y → Y ∈ V