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

Metamath Proof Explorer

Theorem lvolnleat

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

Ref Expression
Hypotheses lvolnleat.l 
|- .<_ = ( le ` K )
lvolnleat.a 
|- A = ( Atoms ` K )
lvolnleat.v 
|- V = ( LVols ` K )
Assertion lvolnleat 
|- ( ( K e. HL /\ X e. V /\ P e. A ) -> -. X .<_ P )

Proof

Step Hyp Ref Expression
1 lvolnleat.l 
 |-  .<_ = ( le ` K )
2 lvolnleat.a 
 |-  A = ( Atoms ` K )
3 lvolnleat.v 
 |-  V = ( LVols ` K )
4 3simpa 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> ( K e. HL /\ X e. V ) )
5 simp3 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> P e. A )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 1 6 2 3 lvolnle3at 
 |-  ( ( ( K e. HL /\ X e. V ) /\ ( P e. A /\ P e. A /\ P e. A ) ) -> -. X .<_ ( ( P ( join ` K ) P ) ( join ` K ) P ) )
8 4 5 5 5 7 syl13anc 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> -. X .<_ ( ( P ( join ` K ) P ) ( join ` K ) P ) )
9 6 2 hlatjidm 
 |-  ( ( K e. HL /\ P e. A ) -> ( P ( join ` K ) P ) = P )
10 9 3adant2 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> ( P ( join ` K ) P ) = P )
11 10 oveq1d 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> ( ( P ( join ` K ) P ) ( join ` K ) P ) = ( P ( join ` K ) P ) )
12 11 10 eqtrd 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> ( ( P ( join ` K ) P ) ( join ` K ) P ) = P )
13 12 breq2d 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> ( X .<_ ( ( P ( join ` K ) P ) ( join ` K ) P ) <-> X .<_ P ) )
14 8 13 mtbid 
 |-  ( ( K e. HL /\ X e. V /\ P e. A ) -> -. X .<_ P )