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