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 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 )