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