Theorem islvol2

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	islvol5.b	|- B = ( Base ` K )
	islvol5.l	|- .<_ = ( le ` K )
	islvol5.j	|- .\/ = ( join ` K )
	islvol5.a	|- A = ( Atoms ` K )
	islvol5.v	|- V = ( LVols ` K )
Assertion	islvol2	|- ( K e. HL -> ( X e. V <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islvol5.b	|- B = ( Base ` K )
2		islvol5.l	|- .<_ = ( le ` K )
3		islvol5.j	|- .\/ = ( join ` K )
4		islvol5.a	|- A = ( Atoms ` K )
5		islvol5.v	|- V = ( LVols ` K )
6	1 5	lvolbase	|- ( X e. V -> X e. B )
7	6	pm4.71ri	|- ( X e. V <-> ( X e. B /\ X e. V ) )
8	1 2 3 4 5	islvol5	|- ( ( K e. HL /\ X e. B ) -> ( X e. V <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
9	8	pm5.32da	|- ( K e. HL -> ( ( X e. B /\ X e. V ) <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
10	7 9	bitrid	|- ( K e. HL -> ( X e. V <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )