Metamath Proof Explorer

Theorem lvolnlelln

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

Ref Expression
Hypotheses lvolnlelln.l 
|- .<_ = ( le ` K )
lvolnlelln.n 
|- N = ( LLines ` K )
lvolnlelln.v 
|- V = ( LVols ` K )
Assertion lvolnlelln 
|- ( ( K e. HL /\ X e. V /\ Y e. N ) -> -. X .<_ Y )

Proof

Step Hyp Ref Expression
1 lvolnlelln.l 
 |-  .<_ = ( le ` K )
2 lvolnlelln.n 
 |-  N = ( LLines ` K )
3 lvolnlelln.v 
 |-  V = ( LVols ` K )
4 simp3 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> Y e. N )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 5 6 7 2 islln2 
 |-  ( K e. HL -> ( Y e. N <-> ( Y e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) ) )
9 8 3ad2ant1 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> ( Y e. N <-> ( Y e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) ) )
10 4 9 mpbid 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> ( Y e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) )
11 simp11 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> K e. HL )
12 simp12 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> X e. V )
13 simp2l 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> p e. ( Atoms ` K ) )
14 simp2r 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> q e. ( Atoms ` K ) )
15 1 6 7 3 lvolnle3at 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( p e. ( Atoms ` K ) /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) -> -. X .<_ ( ( p ( join ` K ) p ) ( join ` K ) q ) )
16 11 12 13 13 14 15 syl23anc 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> -. X .<_ ( ( p ( join ` K ) p ) ( join ` K ) q ) )
17 simp3r 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> Y = ( p ( join ` K ) q ) )
18 6 7 hlatjidm 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) ) -> ( p ( join ` K ) p ) = p )
19 11 13 18 syl2anc 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> ( p ( join ` K ) p ) = p )
20 19 oveq1d 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> ( ( p ( join ` K ) p ) ( join ` K ) q ) = ( p ( join ` K ) q ) )
21 17 20 eqtr4d 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> Y = ( ( p ( join ` K ) p ) ( join ` K ) q ) )
22 21 breq2d 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> ( X .<_ Y <-> X .<_ ( ( p ( join ` K ) p ) ( join ` K ) q ) ) )
23 16 22 mtbird 
 |-  ( ( ( K e. HL /\ X e. V /\ Y e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> -. X .<_ Y )
24 23 3exp 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( ( p =/= q /\ Y = ( p ( join ` K ) q ) ) -> -. X .<_ Y ) ) )
25 24 rexlimdvv 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> ( E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ Y = ( p ( join ` K ) q ) ) -> -. X .<_ Y ) )
26 25 adantld 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> ( ( Y e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ Y = ( p ( join ` K ) q ) ) ) -> -. X .<_ Y ) )
27 10 26 mpd 
 |-  ( ( K e. HL /\ X e. V /\ Y e. N ) -> -. X .<_ Y )