Metamath Proof Explorer

Theorem lvolnlelpln

Description: A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lvolnlelpln.l 
|- .<_ = ( le ` K )
lvolnlelpln.p 
|- P = ( LPlanes ` K )
lvolnlelpln.v 
|- V = ( LVols ` K )
Assertion lvolnlelpln 
|- ( ( K e. HL /\ X e. V /\ Y e. P ) -> -. X .<_ Y )

Proof

Step Hyp Ref Expression
1 lvolnlelpln.l 
 |-  .<_ = ( le ` K )
2 lvolnlelpln.p 
 |-  P = ( LPlanes ` K )
3 lvolnlelpln.v 
 |-  V = ( LVols ` K )
4 simp3 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> Y e. P )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 5 1 6 7 2 islpln2 
 |-  ( K e. HL -> ( Y e. P <-> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) ) )
9 8 3ad2ant1 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> ( Y e. P <-> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) ) )
10 4 9 mpbid 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) )
11 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> K e. HL )
12 simp1l2 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> X e. V )
13 simp1r 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> q e. ( Atoms ` K ) )
14 simp2l 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> r e. ( Atoms ` K ) )
15 simp2r 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> s e. ( Atoms ` K ) )
16 1 6 7 3 lvolnle3at 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) -> -. X .<_ ( ( q ( join ` K ) r ) ( join ` K ) s ) )
17 11 12 13 14 15 16 syl23anc 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> -. X .<_ ( ( q ( join ` K ) r ) ( join ` K ) s ) )
18 simp33 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) )
19 18 breq2d 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> ( X .<_ Y <-> X .<_ ( ( q ( join ` K ) r ) ( join ` K ) s ) ) )
20 17 19 mtbird 
 |-  ( ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> -. X .<_ Y )
21 20 3exp 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) -> ( ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) -> ( ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) -> -. X .<_ Y ) ) )
22 21 rexlimdvv 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. P ) /\ q e. ( Atoms ` K ) ) -> ( E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) -> -. X .<_ Y ) )
23 22 rexlimdva 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) -> -. X .<_ Y ) )
24 23 adantld 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> ( ( Y e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q ( join ` K ) r ) /\ Y = ( ( q ( join ` K ) r ) ( join ` K ) s ) ) ) -> -. X .<_ Y ) )
25 10 24 mpd 
 |-  ( ( K e. HL /\ X e. V /\ Y e. P ) -> -. X .<_ Y )