Theorem lvolbase

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

	Ref	Expression
Hypotheses	lvolbase.b	$$⊢B={\mathrm{Base}}_K$$
	lvolbase.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvolbase	$$⊢X\in V\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		lvolbase.b	$$⊢B={\mathrm{Base}}_K$$
2		lvolbase.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
3		n0i	$$⊢X\in V\to \neg V=\varnothing$$
4	2	eqeq1i	$$⊢V=\varnothing \leftrightarrow \mathrm{LVols}\left(K\right)=\varnothing$$
5	3 4	sylnib	$$⊢X\in V\to \neg \mathrm{LVols}\left(K\right)=\varnothing$$
6		fvprc	$$⊢\neg K\in \mathrm{V}\to \mathrm{LVols}\left(K\right)=\varnothing$$
7	5 6	nsyl2	$$⊢X\in V\to K\in \mathrm{V}$$
8		eqid	$$⊢{⋖}_K={⋖}_K$$
9		eqid	$$⊢\mathrm{LPlanes}\left(K\right)=\mathrm{LPlanes}\left(K\right)$$
10	1 8 9 2	islvol	$$⊢K\in \mathrm{V}\to \left(X\in V\leftrightarrow \left(X\in B\wedge \exists x\in \mathrm{LPlanes}\left(K\right)x{⋖}_{K}X\right)\right)$$
11	10	simprbda	$$⊢\left(K\in \mathrm{V}\wedge X\in V\right)\to X\in B$$
12	7 11	mpancom	$$⊢X\in V\to X\in B$$