Metamath Proof Explorer


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 syl5bb
 |-  ( 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 ) ) ) ) )