# Metamath Proof Explorer

## Theorem lplnric

Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses islpln2a.l
`|- .<_ = ( le ` K )`
islpln2a.j
`|- .\/ = ( join ` K )`
islpln2a.a
`|- A = ( Atoms ` K )`
islpln2a.p
`|- P = ( LPlanes ` K )`
islpln2a.y
`|- Y = ( ( Q .\/ R ) .\/ S )`
Assertion lplnric
`|- ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> -. S .<_ ( Q .\/ R ) )`

### Proof

Step Hyp Ref Expression
1 islpln2a.l
` |-  .<_ = ( le ` K )`
2 islpln2a.j
` |-  .\/ = ( join ` K )`
3 islpln2a.a
` |-  A = ( Atoms ` K )`
4 islpln2a.p
` |-  P = ( LPlanes ` K )`
5 islpln2a.y
` |-  Y = ( ( Q .\/ R ) .\/ S )`
6 1 2 3 4 5 islpln2ah
` |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( Y e. P <-> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) ) ) )`
7 6 biimp3a
` |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) ) )`
8 7 simprd
` |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) /\ Y e. P ) -> -. S .<_ ( Q .\/ R ) )`