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 e. V -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		lvolbase.b	|- B = ( Base ` K )
2		lvolbase.v	|- V = ( LVols ` K )
3		n0i	|- ( X e. V -> -. V = (/) )
4	2	eqeq1i	|- ( V = (/) <-> ( LVols ` K ) = (/) )
5	3 4	sylnib	|- ( X e. V -> -. ( LVols ` K ) = (/) )
6		fvprc	|- ( -. K e. _V -> ( LVols ` K ) = (/) )
7	5 6	nsyl2	|- ( X e. V -> K e. _V )
8		eqid	|- (
9		eqid	|- ( LPlanes ` K ) = ( LPlanes ` K )
10	1 8 9 2	islvol	|- ( K e. _V -> ( X e. V <-> ( X e. B /\ E. x e. ( LPlanes ` K ) x (
11	10	simprbda	|- ( ( K e. _V /\ X e. V ) -> X e. B )
12	7 11	mpancom	|- ( X e. V -> X e. B )