Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | islpln5.b | |- B = ( Base ` K ) |
|
| islpln5.l | |- .<_ = ( le ` K ) |
||
| islpln5.j | |- .\/ = ( join ` K ) |
||
| islpln5.a | |- A = ( Atoms ` K ) |
||
| islpln5.p | |- P = ( LPlanes ` K ) |
||
| Assertion | islpln2 | |- ( K e. HL -> ( X e. P <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | islpln5.b | |- B = ( Base ` K ) |
|
| 2 | islpln5.l | |- .<_ = ( le ` K ) |
|
| 3 | islpln5.j | |- .\/ = ( join ` K ) |
|
| 4 | islpln5.a | |- A = ( Atoms ` K ) |
|
| 5 | islpln5.p | |- P = ( LPlanes ` K ) |
|
| 6 | 1 5 | lplnbase | |- ( X e. P -> X e. B ) |
| 7 | 6 | pm4.71ri | |- ( X e. P <-> ( X e. B /\ X e. P ) ) |
| 8 | 1 2 3 4 5 | islpln5 | |- ( ( K e. HL /\ X e. B ) -> ( X e. P <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) |
| 9 | 8 | pm5.32da | |- ( K e. HL -> ( ( X e. B /\ X e. P ) <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) ) |
| 10 | 7 9 | syl5bb | |- ( K e. HL -> ( X e. P <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) ) |