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 )