This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lvolnltN

Description: Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolnlt.s 
|- .< = ( lt ` K )
lvolnlt.v 
|- V = ( LVols ` K )
Assertion lvolnltN 
|- ( ( K e. HL /\ X e. V /\ Y e. V ) -> -. X .< Y )

Proof

Step Hyp Ref Expression
1 lvolnlt.s 
 |-  .< = ( lt ` K )
2 lvolnlt.v 
 |-  V = ( LVols ` K )
3 1 pltirr 
 |-  ( ( K e. HL /\ X e. V ) -> -. X .< X )
4 3 3adant3 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> -. X .< X )
5 breq2 
 |-  ( X = Y -> ( X .< X <-> X .< Y ) )
6 5 notbid 
 |-  ( X = Y -> ( -. X .< X <-> -. X .< Y ) )
7 4 6 syl5ibcom 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> ( X = Y -> -. X .< Y ) )
8 eqid 
 |-  ( le ` K ) = ( le ` K )
9 8 1 pltle 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> ( X .< Y -> X ( le ` K ) Y ) )
10 8 2 lvolcmp 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> ( X ( le ` K ) Y <-> X = Y ) )
11 9 10 sylibd 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> ( X .< Y -> X = Y ) )
12 11 necon3ad 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> ( X =/= Y -> -. X .< Y ) )
13 7 12 pm2.61dne 
 |-  ( ( K e. HL /\ X e. V /\ Y e. V ) -> -. X .< Y )